COMMENT ⊗   VALID 00034 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00004 00002	\input basic
C00008 00003	\output{\baselineskip 18pt\page}
C00010 00004	\parskip .15in plus 5pt \baselineskip 15pt \lineskip 1pt
C00012 00005	\ctrline{RESEARCH AND DEVELOPMENT}
C00040 00006	\ctrline{BASIC RESEARCH}
C00044 00007	\sect Formal Reasoning.
C00075 00008	\sect Advice-taking ANALYST.
C00116 00009	\sect Formalisms for Reasoning about Programs.
C00153 00010	\sect EKL.
C00160 00011	\sect Lisp Performance Evaluation.
C00164 00012	\sect Common Lisp.
C00174 00013	\sect Automatic Construction of Special-purpose Programs.
C00197 00014	\sect Epistemology and Formalization of Concurrent and Continuous Action.
C00201 00015	\sect Proving Facts About Lisp.
C00204 00016	\sect Background.
C00209 00017	\sect References.
C00220 00018	\ctrline{DEDUCTIVE PROGRAMMING}
C00255 00019	\sect References.
C00259 00020	\ctrline{RESEARCH IN THE ANALYSIS OF ALGORITHMS}
C00269 00021	%Data Base Research
C00278 00022	\sect Previous Work.
C00286 00023	\ssect A methodology for the design of user models.
C00292 00024	\ssect Update of data.
C00305 00025	\ssect Task models.
C00310 00026	\ssect Descriptive responses to database queries.
C00347 00027	\sect Transfer to DOD.
C00353 00028	\sect Reports and Papers.
C00374 00029	%Programming Analysis and Verification
C00398 00030	\sect References.
C00419 00031	%Analysis of Algorithms
C00424 00032	%Vision and Robotics
C00462 00033	\sect References.
C00477 00034	%Table of Contents
C00479 ENDMK
C⊗;
\input basic
\jpar 1000
\varunit 1truein
\parskip .15in plus 5pt \baselineskip 15pt \lineskip 1pt
\def\rm{\:a} \def\sl{\:n} \def\bf{\:q} \def\it{\:?}
\font m=cmsc10 		%  Small caps
\def\sc{\:m}		%  Small Caps  (10pt)
\font p=cms8
\font s=cmb8
\font c=cmr8
\font N=cmdunh		%  Titles
\font M=cmb12 		%  Titles
\font <=cmb10		%  Bolder
\font t=cmtt9[tex,sys]
%\output{\advcount0\baselineskip 18pt\page}
\def\sect#1.{\vskip 20pt plus20pt minus 7pt\penalty -100
   \secta#1.}
\def\secta#1.{\noindent{\bf \count1.\quad #1}\par\penalty 1000\advcount1\par
\vskip 5pt plus4pt minus 3pt\penalty 1000}

\def\eightpoint{\baselineskip9.5pt
  \def\rm{\:c} \def\sl{\:p} \def\bf{\:s}
  \rm}

\setcount1 1
\def \initsect{\setcount1 1\baselineskip 15pt}
\setcount0 1
\setcount2 0
\def\footnote#1{\advcount2\ofootnote{\count2}{#1}}

\def\ofootnote#1#2{{\eightpoint$↑{\hbox{#1}}$}\botinsert{\vskip 12pt 
	plus 10pt minus10pt \baselineskip 10pt\hbox par 6.5truein{\eightpoint
	\raise 4pt\hbox{#1}\hskip 2pt #2}}} 

\def\ssect#1.{\yyskip{\bf\penalty -50\hbox{\vbox{\hbox{#1}}}
\penalty 800}} 
\def \ni{\noindent}

\def\textindent#1{\noindent\hbox to 19pt{\hskip 0pt plus 1000pt minus 1000pt#1\ 
\!}}
\def\hang{\hangindent 19pt}

\def\numitem#1{\yskip\hang\textindent{#1}}

\def\ref:#1.#2.{[\hbox{#1 #2}]}

\def	\bcode	{\par\vfil\penalty400\vfilneg\parskip 0pt plus 1 pt\vskip .25 in\: t\beginpassasis}
\def	\ecode  {\endpassasis\: a\par\vskip .05 in\vfil\penalty500\vfilneg\parskip .1 in plus 5pt}

\input pai[can,rpg]

\def\eat#1\endeat{}	% macro for extended comments
\def\makeref:#1.#2.#3{\par{\noindent \parshape 2 0truein 6.5truein
.5truein 6.0truein \hbox{[\hbox{#1 #2}]}\linebreak 
{#3}}\par\parshape 0\vfil\penalty 0\vfilneg}
\def\article#1{{\sl #1}}
\def\book#1{{\:< #1}}
\def\yyskip{\penalty-100\vskip8pt plus6pt minus4pt}
\def\yskip{\penalty-50\vskip 3pt plus 3pt minus 2pt}
\def\bslskp{\baselineskip 15pt}
\def\dispskip{\vskip12pt plus 10pt minus 5pt}
\def\bite{\noindent $\bullet$\ }
\def\Hpar#1{\par\parshape 2 .2truein 6.3truein .5truein 6.0truein #1\par\parshape 0}
\def\HHpar#1{\par\parshape 2 0truein 6.0truein .5truein 5.5truein #1\par\parshape 0}
\def\BBpar#1{\numitem{$\bullet$}#1}
\def\lead{\leaders\hbox to 10pt{\hfill.\hfill}\hfill}
\def\contents#1#2{\hbox to size{#1\lead #2}}
\output{\baselineskip 18pt\page}
\:M
\baselineskip 18pt
\ctrline{Proposal to}
\ctrline{The Defense Advanced Research Projects Agency}
\ctrline{for}
\ctrline{Research and Development in Computer Science}
\vfill
\ctrline{John McCarthy}
\ctrline{Professor of Computer Science}
\vfill
\ctrline{Zohar Manna}
\ctrline{Professor of Computer Science}
\vfill
\ctrline{Donald E. Knuth}
\ctrline{Professor of Computer Science}
\vfill
\ctrline{Gio Wiederhold}
\ctrline{Assistant Professor of Computer Science}
\vfill
\ctrline{David C. Luckham}
\ctrline{Professor of Electrical Engineering (Research)}
\vfill
\ctrline{Gene Golub}
\ctrline{Professor of Computer Science}
\vfill
\ctrline{Thomas Binford}
\ctrline{Professor of Computer Science (Research)}
\vfill
\ctrline{April 1983}
\:M
\ctrline{Departments of Computer Science and Electrical Engineering}
\ctrline{Schools of Humanities and Sciences, and Engineering}
\ctrline{Stanford University}
\vfill\eject
\parskip .15in plus 5pt \baselineskip 15pt \lineskip 1pt
\output{\baselineskip 18pt\page\ctrline{\curfont a\count0}\advcount0}
\rm
\ctrline{RESEARCH AND DEVELOPMENT}
\vskip .2truein
\ctrline{IN}
\vskip .2truein
\ctrline{COMPUTER SCIENCE}
\vskip .2truein

\sect General Introduction.
\save0\hbox{\count0}

Computer science as a field is difficult to define, being tied intuitively
to a body of machines, artifacts of humanity. There are, though, some
common threads that join most people working in this field. We are
concerned with making the computer, as a tool, as powerful and as easy to
use as we can. We want to increase the simplicity of telling the computer
what it is that we want it to do, what it should do. 

The Computer Science Department of Stanford University will continue to
lead the way, using the unique expertise that it has acquired and nurtured
over the years.  This proposal indicates the ways that we feel that
Stanford University can help further the goals of computer science and of
science in general. Our proposal centers on Research and Development in
computer science, to replenish and enhance the stock of ideas that
everyone who deals with computers and with computers must draw from, and
to apply these ideas to problems common to the community in ways useful to
DARPA/NAVALEX.

These directions will form the basis on which Stanford
University will enter into a tasking relationship with DARPA/NAVELEX.
These tasks will be structured to define precisely the objectives,
expectations, and available resources to attack the problems
within the scope indicated here.

\ssect Outline.

Section 2 outlines general scope of the proposal.  Section 3 is a summary
of current research directions; it provides some specific examples of
problems being addressed within that scope.  The remainder of the document
provides background and qualification information to demonstrate our
capabilities and research record.

A budget to delimit the resources required for this research in presented
in Appendix A.  We expect this proposal to become further refined through
individual tasking statements to be attached to this proposal.

\sect The Proposal.

Our proposal is to further the boundaries of computer science along the
lines laid out below.  The proposed research spans the range from
theoretical investigations to extend the foundations of analytic computer
science and artificial intelligence to experiments in the application of
the results to challenging problems in the design and operation of
advanced computer hardware and software.  The unique qualifications which
Stanford University brings to this research are outlined in a section
below.

Research in the fundamental areas of computer science will study the
principles underlying human and machine reasoning.  Formal languages will
be developed and utilized to capture the processes and constraints as
nearly exactly as feasible.  Language processors and other computer
software for will be designed to be portable to support modern concepts of
hybrid systems composed of workstations and supercomputers.  In this
environment we will also find distributed knowledge and databases.  We
will search for new approaches to deal with the complexity and size of the
structures required to represent the information in such systems.

We propose research to simplify the tasks of programming by providing
automatic deduction of programs from specifications and to provide
tools for the analysis and verification of such programs which cannot
be automatically generated.

We propose to improve the computational task by studying algorithmic
techniques and considering how they can be exploited by improved
computer architectures.

The remainder of this document outlines some of the
research directions that the computer science Department has been doing
recently as well as state some examples of goals and directions that
we feel may be positive first steps towards such research and development.

\sect Previous and Current Work in Computer Science at Stanford.

This statement of background describes the recent research and current
directions of the Formal Reasoning; Vision and Robotics; Database;
Deductive Programming; Program Analysis and Verification; and Analysis of
Algorithms groups in the Computer Science Department at Stanford
University.  As such it indicates also the immediate directions being
considered for our research, since we plan to build on the invaluable
experience obtained which is available in our institution and through our
collegues.  Being a broad statement it covers a spectrum of areas and
problems; these areas are presented separately with a bibliography in each
section.

\ssect Formal Reasoning.

Formal Reasoning is a methodology for studying the basic modes of thought,
decision-making, planning, and reasoning that people use in both their everyday
lives and in their roles as computer programmers. This methodology makes
explicit and simple the objects that fill the world as well as the
properties they have and the relations between them. The representation
used is either first-order predicate calculus or one of the well-studied
variants of it. In this way the issues of belief, knowledge, ignorance,
and epistemology are at the surface of attention rather than buried beneath
{\sl ad hoc} representations. Since these logical languages have a well-known
semantics there is never any doubt about meaning.

These techniques are applied to artifical intelligence problems, to the
study of the mathematical theory of computation, to specialized automatic
programming, and to programming languages.

\ssect Lisp.

Lisp has been and continues to be the primary language for artificial
intelligence research. Increasingly it is used as a systems language:
operating systems and compilers now being routinely written in Lisp. Since
Lisp requires a runtime system, and since the semantics of the language
are not operational semantics, neither the tactics nor the strategy of
implementation for most facets are pre-determined.  For instance, there is
no statement of the requirement for either deep-binding or shallow-binding
for variables. Therefore there is much room for experimentation with the
most effective strategies and tactics for implementation of Lisp given
specific machines and applications.

Due to the variations in implementation strategies, performance evaluation
is a difficult problem for Lisp systems.  Programming styles and even the
types of problems attacked are affected by the available Lisp systems and
vice versa. Understanding the facets of performance in the Lisp context
would provide much information about the programming process.

Since Lisp technology has matured over the years and since there seems to
be a rapid growth in the number and variety of computers available, the
need for portable Lisp implementations based on a rich dialect has become
increasingly apparent. Moreover, this variety in architectures provides
the basis for an argument that portable compilers must be able to exploit
these architectures, and that this must be accomplished by exploiting
the best compiler technologies available. A portable Lisp must be able to
run well on personal computers, supercomputers, and multiprocessors.

Being a programming system as well as simply a programming language,
a programming environment is necessary for the success and usefulness
of a Lisp implementation. A portable Lisp implementation requires a
portable Lisp environment.

Lisp programmers tend to be the most intensive users of a computer system,
and the large programming environment and the use of a heap for storage
allocation put a heavy load on the resources provided by the hardware and
operating system.  Effective program development demands efficient use of
these resources, so it is productive to study the effects of the structure
of an operating system on the number of Lisp and other users that can be
supported in various parts of the program development cycle and in the
interactions typical of AI research.

Because Common Lisp has been widely accepted by the Lisp and
artificial intellegence communities, it is the most attractive Lisp dialect
for this portability.

\ssect Software.

While it is true that the average programmer or computer user consumes few
resources in his typical use, there are applications and problems that
require extreme processing power. Thus it is necessary to look at both
personal workstations linked by a communications network for `normal'
computing needs as well as at supercomputers (uniprocessors and
multiprocessors) to provide the tools that scientists, engineers,
businessmen, and the military need.

High-performance and multiprocessed computers present special problems in
terms of software, especially operating systems. These problems arise
since the ability to execute instructions rapidly often requires a
non-uniform architecture (special registers, vector representations, etc),
a complex instruction set (to take advantage of internal
parallelism---increasing the work per instruction), complex addressing
modes, or non-uniform memory hierarchies. Some high-performance
architectures use simple data paths and simple addressing modes to
increase performance by decreasing the amount of overhead per instruction
fetch and decode. Nevertheless, writing compilers, for example, for such
complex machines requires matching tasks to instructions or instruction
sequences, which is often difficult.  Beyond this any multiprocessing is
an added problem.

Developing tools and techniques for the effective use of complex
supercomputers and large networks of computers is the next important step
for systems research.\footnote{Under separate contracts principal
investigators participating in this project have performed research and
developed software for a high-performance multiprocessor, the S-1 system
at Lawrence Livermore Laboratories.  Such work has included a basic
operating system, a language translation system including as modules
several compilers, optimizers, code-generators, an interpreter, and linker
and loaders.  A portable file system, developed initially under joint
sponsorship, is intended to help manage the large data quantities expected
when systems as the S-1 reach full operation.  Important research results
of this work include experience in developing software which is more
modular than previous systems, so that improvements in software technology
can be more rapidly moved to evolving computer systems.  High-performance,
low quantity systems present important issues of software design of which
we will be conscious in our research plans.}

\ssect Database Management and the Use of Knowledge.

To be effective computers must be able to store large amounts of data
in ways that are flexible, expandable, and convenient for the types
of processing required on that data. Centralized and distributed data bases
are appropriate for different settings. The management of large quantities of
data cannot be solved by algorithmic methods 
alone: in many cases the techniques required to process data are heuristic. 
The architecture of computers that are designed for these applications 
may not resemble standard Von Neumann machines.

Thus Database Management stands in a unique position of drawing deeply
from all aspects of computer science to achieve its goals.

\ssect Deductive Programming.

Programmers working on their task can often state clearly what they want
their program to do without being to state clearly how that can be
achieved. In many cases it may be possible to transform high-level,
mathematical statements of the specifications for a program into code that
is reasonably efficient to execute.  There are several approaches to this
transformation, but one that seems particularly attractive is to turn the
specification into a mathematical theorem stating the existence of a
function that achieves te specification.  By constructively proving that
theorem one can often determine enough information to derive a program
that realizes the specification.  To be more specific, a program can be
thought of as a (partial) function that takes a particular input as an
argument and produces a particular output as a value.  The value must
satisfy a given predicate or be in some relation to the input.  A suitable
mathematical theorem would state the existence of that function.  A
constructive proof would find such a function, and care in that proof
could also produce a program.

The importance of a technique or system that accomplished this goal is that
it would place programming in the realm of stating a correct specification for
the effect of the program in a language that is well-suited to such a
clear specification. Moreover it would produce a provably correct program for
the specification: no debugging would be required.

\ssect Research and Development in Advanced Programming Environments.

Software engineering is concerned with providing languages, techniques, and
tools that enable programmers to produce reliable high quality software
efficiently.  It addresses the widely recognized problems of systems being
too costly to produce and unreliable in operation.  Software engineering
is developing a new technology for coping with these problems within
the context of the increasing complexity of modern systems.  This
complexity increase, together with a greater demand for new systems than
ever before and a general shortage of skilled personnel, is having the
effect of magnifying the cost, reliability, and quality problems.  The
situation has now reached a point where it is often referred to as ``the
software crisis.''

The major goal of recent research in Software Engineering is to apply
automated techniques to all stages of the software life cycle:
requirements, specification, implementation, and maintenance. This
direction results from a general acceptance that the most promising
approach to solving the software crisis is the development and adoption of
advanced knowledge-based software tools.  Therefore much recent research
effort has focused on three basic areas:

\numitem{(1)}{\bf Languages:} development of
new machine-processable languages for support of systems production
activities other than implementation (e.g.  formal requirements,
specification, and documentation languages), 

\numitem{(2)}{\bf Programming Environments:}
the design and implementation of tools based on the new languages for the
support of systems production and the integration of sets of tools into
programming environments, and 

\numitem{(3)}{\bf Methodology:} development of new
methodology of software production utilizing advanced automated tools and
emphasizing such factors as reliability and reuseability.  

Of particular concern within each of these three areas are the problems
posed by new complex systems that utilize concurrent and distributed
processing.  

\ssect The Analysis of Algorithms.

The study of computer science centers on computers and on algorithms.

The study of computers, {\sl per se}, centers on creating new
architectures and hardware is the most visible activity of computer
science. With new hardware new problems can be attacked which were
previously either beyond the computational capabilities of older hardware
or beyond the economic grasp of the people needing the solutions.

The study of algorithms has three main goals:  to create efficient new
computer methods for important practical problems; to create better
mathematics in order to determine how efficient such methods are; and to
extend programming methodology so that such algorithms can be implemented
more quickly and reliably than with current techniques.  

In many cases these studies are not conducted together, and it often
happens that the design of computers takes place without direct experience
with the intended applications of those computers.  It may be possible to
understand the scope and computation/communications needs of a problem of
application before much algorithmic development has taken place. With a
gauge of the problem and its requirements it would be possible to obtain a
better match between application and hardware than is currently possible
and typical.

\ssect Intelligent Systems for Computer Vision and Robotics.

Intelligent systems which interact in the real-world take input from the
world, plan actions, and act on the world, that is, sensing, intelligence, and
action.  An intelligent system monitors and controls actions of its
effectors; one action is to gather information actively by controlling
sensor input, as in eye motion and exploration with tactile sensors.

Intelligence includes several aspects.  Perception transforms the input
data of sensors into information about space/time states (behavior) of
objects, using representations to abstract observations into compact
space/time models.  Learning and memory mechanisms exploit unique,
identifiable, and consistent structure to store and retrieve space/time
models.  Planning mechanisms reason from models of behavior as transition
rules to use in choosing actions which move from a class of initial states
to a class of goal states.

\vfill\eject
\ctrline{BASIC RESEARCH}
\vskip .2truein
\ctrline{IN}
\vskip .2truein
\ctrline{ARTIFICIAL INTELLIGENCE}
\vskip .2truein
\ctrline{AND}
\vskip .2truein
\ctrline{FORMAL REASONING}

$$\vcenter{\halign{\lft{#}\cr
John McCarthy, Professor\cr
Computer Science Department\cr
Stanford University\cr}}$$
 
\vskip 30pt

\vfill

\initsect

\sect Introduction.
\save1\hbox{\count0}

Applied research requires basic research to replenish the stock of ideas
on which its progress depends.  The long range goals of work in basic AI
and formal reasoning are to make computers carry out the reasoning
required to solve problems.  Our work over the past few years has made it
considerably clearer how our formal approach can be applied to AI and MTC
problems.  This brings application nearer, especially in the area of
mathematical theory of computation.

The rest of this section will discuss the recent research of the people
in the Formal Reasoning Group and their long-term research interests and
directions. The work of this group during the next 3--5 years will be
along these lines.

\sect Formal Reasoning.

\ssect Accomplishments.

John McCarthy continued his work in formalization
of the commonsense facts about the world needed for intelligent
behavior and also work in formalization of computer programs.

McCarthy's personal research concerns the formalization of commonsense
knowledge and commonsense reasoning in mathematical/logical languages.
Such formalization is required to represent the information in the memory
of a computer and to make programs that can reason with the information in
order to solve problems.  It is now widely agreed (for example, by
Newell, Nilsson, and Minsky) that progress in artificial intelligence is
limited by our ability to express commonsense knowledge and reasoning.
There isn't widespread agreement on how to do this, and McCarthy's work
explores one end of the spectrum of ideas---using mathematical logic.

	Since 1981, McCarthy made substantial progress on three
problems:

\ni 1. Non-monotonic reasoning.

	In 1980 McCarthy published ``Circumscription: a method
of non-monotonic reasoning.''  Since that time circumscription
has been further developed.  A forthcoming paper will describe
a new formalization and many new applications.

There seem to be many kinds of non-monotonic reasoning formalizable by
circumscription, and it isn't clear how to unify them.  It also isn't
clear whether circumscription is a universal form of non-monotonic
reasoning or whether other forms will be required.  Circumscription is
known to subsume many examples of non-monotonic reasoning given earlier by
McDermott and Doyle, and by Reiter; and there are no outstanding cases
where it is not known how to do it.

	Here are some example uses of circumscription.

\numitem{a.}As a communication convention.  Suppose  A  tells  B  about
a situation involving a bird.  If the bird may not be able to fly, and this
is relevant to solving the problem, then  A  should mention
the relevant information.  Whereas if the bird can fly, there is
no requirement to mention the fact.

\numitem{b.}As a database or information storage convention.  It can be a
convention of a particular database that certain predicates have their
minimal extension.  This generalizes the closed-world assumption of
Reiter.  When a database makes the closed-world assumption for all
predicates it is reasonable to imbed this fact in the programs that use
the database.  However, when there is a priority structure among the
predicates, we need to express the priorities as sentences of the
database, perhaps included in a preamble to it.

\numitem{}Neither 1 nor 2 requires that most birds can fly.  Should it happen in
situations 1 and 2 above that most birds cannot fly, the convention may
lead to inefficiency but not incorrectness.

\numitem{c.} As a rule of conjecture.  This use was emphasized in
\ref:McCarthy.1980..  The circumscriptions may be regarded as expressions
of some probabilistic notions such as `most birds can fly' or they may be
expressions of simple cases.  Thus it is simple to conjecture that there
are no relevant present material objects other than those whose presence
can be inferred.  It is also a simple conjecture that a tool asserted to
be present is usable for its normal function.  Such conjectures sometimes
conflict, but there is nothing wrong with having incompatible conjectures
on hand.  Besides the possibility of deciding that one is correct and the
other wrong, it is possible to use one for generating possible exceptions
to the other.

\numitem{d.}As a representation of a policy.  The example is Doyle's ``The meeting
will be on Wednesday unless another decision is explicitly made.''

\numitem{e.}As a very streamlined expression of probabilistic information when
numerical probabilities, especially conditional probabilities, are
unobtainable.  Since circumscription doesn't provide numerical
probabilities, its probabilistic interpretation involves probabilities that
are either infinitesimal, within an infinitesimal of one, or
intermediate---without any discrimination among the intermediate values.
Circumscriptions give conditional probabilities.  Thus we may treat
the probability that a bird cannot fly as an infinitesimal.  However, if
the rare event occurs that the bird is a penguin, then the conditional
probability that it can fly is infinitesimal, but we may hear of some rare
condition that would allow it to fly after all.

\numitem{}Why don't we use finite probabilities combined by the usual laws?  That
would be fine if we had the numbers, but circumscription is usable when we
can't get the numbers or find their use inconvenient.  Note that the
general probability that a bird can fly may be irrelevant, because we are
interested in particular situations which weigh in favor or against a
particular bird flying.

\numitem{}Notice that circumscription does not provide for weighing evidence; it is
appropriate when the information permits snap decisions.  However, many
cases nominally treated in terms of weighing information are in fact cases
in which the weights are such that circumscription and other defaults work
better.  

\ni 2. Formalization of knowledge about knowledge.
The importance of representing knowledge about knowledge is discussed
elsewhere in this proposal and our previous proposals.  In particular,
the proposed `intelligence analyst' requires knowledge about
knowledge.

McCarthy developed a first-order language that admits Kripke-style
possible worlds as objects and uses the Kripke accessibility relation to
formalize the knowledge that a person has of the value of an expression.
McCarthy showed how to use this formalism to express the facts of a
difficult mathematical puzzle involving knowledge---the following puzzle
of `Mr. S and Mr. P.'

	Two numbers are chosen between 2 and 99 inclusive.  Mr. P
is told the product and Mr. S is told the sum.  The following
dialog occurs:

\ni Mr. P: I don't know the numbers.

\ni Mr. S: I knew you didn't know them.  I don't know them either.

\ni Mr. P: Now I know the numbers.

\ni Mr. S: Now I know the numbers.

\ni Problem: What are the numbers?

\ni Answer: The numbers are 4 and 13.

	The key difficulty to formalizing `Mr. S and Mr. P' comes from
the need to represent ignorance.  How do we represent the facts that
all Mr. S initially knows about the numbers is given by his knowledge
of the sum and that all he knows about Mr. P's knowledge is that Mr.
P knows the product?  Representation of this ignorance is accomplished
by asserting the existence of a sufficiently comprehensive collection
of possible worlds accessible to Mr. S.  Using the possible worlds
in the language itself rather than regarding them as metalinguistic
devices has been uncongenial to logicians.  However, none of the experts on
modal logic to whom the problem has been submitted were able to
formulate it directly in modal logic.

This example problem attracted our attention to an issue that is
fundamental to all programs that reason about knowledge---the
representation of ignorance.  Thus the advice-taking ANALYST (discussed
below) program may conjecture that all the Russians should know about a
certain radar is what can be deduced from its appearance, where it is
used, and the articles in Aviation Week.  We can express this by saying
that any plausible conjecture compatible with this information is a
possibility for them.  If they behave so as to rule out such a
possibility, then we conjecture that they have an additional source of
information.  The explicitly Kripkean formalization developed in
connection with `Mr. S and Mr. P' should work here as well.

	McCarthy's formalization of `Mr. S and Mr. P' was modified
by Ma Xiwen, a Chinese visitor, and used for an FOL proof that
transformed the problem into a purely arithmetic problem.  Unfortunately,
McCarthy found an error in Ma's axioms, and it isn't clear that
when the error is fixed, the proof still works.  Also the axioms
describing the effect of learning---what happens when Mr. P
learns that Mr. S knew he didn't know the numbers---seem to have
some defects.  Formalizing the effect of learning that other people
know something (or do not) is required for making the ANALYST program
work and in any program with similar capabilities.

\ni 3. Introspection in logic programming.  In the early 1970's Alain
Colmerauer of Marseilles University in France and Robert Kowalski of
Imperial College in London proposed the use of first order logic as a
programming language, and the Marseilles group subsequently embodied these
ideas in a programming language called Prolog.  Prolog has become popular
in Europe for artificial intelligence use, and the Japanese `Fifth
Generation' project proposes to use logic programming.  Of people who have
used both Lisp and Prolog, some prefer one and some the other.  Alan
Robinson and others have tried to develop languages that allow both styles
of programming.  McCarthy has tried Prolog and still prefers Lisp.

However, certain issues of programming style come up more clearly in
Prolog than in Lisp.  One of these can be called `introspection,' wherein
a program uses itself and its memory state as data.  This is similar to
`reflection' as studied by Brian Smith in his well-known Harvard PhD
thesis.

Kowalski proposed a slogan
``$\hbox{Algorithm}=\hbox{logic}+\hbox{control}$,'' and proposed that
Prolog permitted a neat separation.  McCarthy has investigated this claim
using a map-coloring logic program devised by Luis Pereira and Antonio
Porto of the University of Lisbon in Portugal.  He noted that two
efficient algorithms for map coloring could be regarded as having the same
logic as the original Pereira-Porto logic program but more sophisticated
control.

One of these algorithms involved a `postponement heuristic' that
re-ordered goals so that goals that could still be realized regardless of
how the previous goals were achieved were put last.  In the map-coloring
case, after some goals have been postponed, still others become
postponable; this process can be repeated.

	The second algorithm uses so-called Kempe transformations
to modify assignments already made to variables when the algorithm
gets stuck.  It is far superior to backtracking for map-coloring,
but it can still be described as control applied to the original
Pereira-Porto logic.  However, this kind of control requires that
the program, when stuck, go into an `introspective mode' wherein
it looks at data structures created by the interpreter that are
not ordinarily accessible to the program itself.  This is the
work whose ideas overlap those of Brian Smith.  Smith applied them
to Lisp, but has recently been exploring the idea that they are
even more applicable to a logic programming language such as
Prolog.

	The two kinds of introspection can be called syntactic
and semantic.  The postponement heuristic is syntactic in that
it involves looking at the goals and re-ordering them before
attempting to realize any of them.  The Kempe heuristic is
semantic in that it doesn't re-order the goals, but modifies
the order in which alternatives are tried in a task-dependent
manner and requires that the program look at its own stack
of tasks.

	McCarthy's results show that in this case the Kowalski
doctrine can be maintained in the map-coloring case.  Both algorithms
can be regarded as sophisticated control applied to simple logic.
The control mechanisms required in the two cases go far beyond
what the logic programmers---for example, Keith Clark, Pereira and Porto,
and Herve Gallaire---had been willing to contemplate.  While they
have some generality it seems likely that additional problems
will require additional mechanism.

	So far it hasn't proved especially convenient to program
by beginning with a simple logic and adding a sophisticated control.
However, such techniques should make it easier to prove the
correctness of programs.  Further exploration of the Kowalski
doctrine applied to logic programming may turn up interesting
and useful methods of control and other heuristics.

\ref:McCarthy.1982. ``Coloring Maps and the Kowalski Doctrine''
presents some of these ideas.

\sect Advice-taking ANALYST.

Lewis Creary and Richard Gabriel are collaborating (Creary full-time, Gabriel
quarter-time) on implementing a prototype version of the advice-taking ANALYST
program.  The motivation, design criteria, basic approach, and leading ideas
for this program were described fully in our previous proposal (1981) and will
not be repeated in detail here.  To summarize briefly, the basic goal of the
project is to construct an advanced, advice-taking problem solver for
analyzing interesting kinds of ``intelligence'' information---in short, a
first incarnation of the ``intelligence'' ANALYST mentioned in our 1979
proposal as a potential long-range application.  This program will attempt to
infer concealed facts from known facts and from reasonable conjectures that it
has made.  It will deal with information about beliefs, desires, purposes,
preferences, aversions, and fears.  It will ascribe plans and goals to people
on the basis of their observed actions and commonsense background knowledge,
and it will use these ascribed plans and goals to predict future actions.  Our
basic approach to construction of an ANALYST stems from John McCarthy's design
sketch for an ``Advice Taker'' \ref:McCarthy.1959. and presently is based on
the following main ideas:

\ni 1. A general framework for the structuring, description, acquisition, and
use of specialized knowledge as the foundation for a domain-independent
commonsense problem solver.  Some of the specialized knowledge will concern
the application domain, and some will be meta-knowledge concerning the
structure, capabilities, etc. of the ANALYST program itself.

\ni 2. Integration of the frames/units and predicate calculus approaches to
knowledge representation.

\ni 3. Extension of the standard predicate calculus formalism to permit
representation of adverbial constructions, sortal quantifiers, information
concerning beliefs, desires and intentions, causal connections between states
of affairs, subjunctive conditional statements, and $λ$-abstraction.

\ni 4. Fregean representation of propositional attitudes, coupled with the
simulative use of the program's own human-like thought mechanisms as a means
of recognizing and analyzing the beliefs, desires, plans, and intentions of
people and other intelligent organisms.

\ni 5. An {\sl interacting considerations} model of commonsense factual
reasoning, in which reasoning involves the weighing and composition of all
reasonably discoverable considerations bearing on a set of target
propositions as the basis for drawing conclusions.

\ni 6. Comparative partial matching as the basis for selection of the most
appropriate methods, procedures, and abstract plan schemata during problem
solving.

\ni 7. Interactive advice seeking and taking as a means of knowledge acquisition.

\ssect Accomplishments.

\ni 1. A new logical language was designed for use by the ANALYST to
represent commonsense information.

An essential requirement for effective commonsense reasoning and
problem-solving is the ability to represent commonsense knowledge about the
everyday world in a way that accurately reflects its logical consequences.
Providing such an ability has not proved easy for AI researchers, since the
standard predicate calculus and its higher-order relatives, while sufficient
for most mathematical purposes, do not lend themselves in a natural way to the
representation of several important types of commonsense proposition.  On the
other hand, while non-logical ad-hoc representation schemes can be effective
in special cases, they tend to lack the flexibility and generality needed for
commonsense reasoning, and needlessly forego the benefits of a systematic
truth-semantics that are available to logically-oriented representation
schemes.

To meet this problem a new logical language named NFLT was designed as the
``thought-vehicle'' for the advice-taking ANALYST.  `NFLT' is an acronym for
`Neo-Fregean Language of Thought.'  NFLT is the result of augmenting and
partially reinterpreting the standard predicate calculus formalism to permit
representation of adverbial constructions; sortal quantifiers; information
concerning beliefs, desires, and intentions; causal connections between states
of affairs; subjunctive conditional statements; and $λ$-abstraction.  Many
commonsense descriptions that are difficult or impossible to express
adequately in the standard predicate calculus are expressible directly and
naturally in NFLT.  While NFLT is much closer semantically to natural language
than is the standard predicate calculus, and is to some extent inspired by
psychologistic considerations, it is nevertheless a formal logic admitting of
a model-theoretic semantics.  The intended semantics incorporates a Fregean
distinction between sense and denotation, with associated principles of
compositionality.  A working paper was written which describes this language
\ref:Creary.1982..  Here is a relatively short example of NFLT's expressive power:

\ni English:

\numitem{}Being careful not to move anything else on his desk, John picks
up $\hbox{hammer}↓1$ with his right hand in order to drive a nail with it.

\ni NFLT Display Syntax:

\bcode
$\{∃$ $\up$X.CONCEPT($\up$X, OF:!DESK JOHN)
   $\up$Y.CONCEPT($\up$Y, OF:HAMMER1)
    Z.NAIL
  $\up$X1.CONCEPT($\up$X1, OF:Z)$\}$.PICKUP(JOHN, HAMMER1, FROM:!DESK JOHN,
 WITH:!RIGHT-HAND JOHN, INORDERTHAT:$\up$[DRIVE(I, $\down$[$\up$X1],
 WITH:$\down$[$\up$Y])], WITHCARETHAT:$\up$[$\{∀$Y1.PHYSOB Y1 $∧$
 ON(Y1, $\down$[$\up$X]) $∧$ $¬$(Y1 $= ¬\down$[$\up$Y])$\}$.$¬$MOVE(I, Y1)])
\ecode
\ni (Here, the `$\down$' operator (occurring within the scope of an `$\up$'
operator) locally suppresses further conceptual raising of the variable it
governs, much as the MacLisp `,' (occurring within a backquote construction)
locally suppresses quotation of the S-expression it governs.)

\ni 2. MacLisp programs were written for the translation, display, and logical
analysis of NFLT formulas, and for the construction and management of a
``uniquifying'' discrimination net that stores all NFLT formulas.

The internal syntax of NFLT is variable-free and has many of the features
of semantic-network formalisms.  For input purposes only a somewhat
different Lisp-form syntax is presently used.  This is translated
immediately upon entry into the internal formalism.  For display purposes
only still another syntax is used, this one being more concise and much
more easily readable by people than the internal syntax, and it is closer
to standard logical notation than the input syntax.  Thus NFLT is
presently implemented with three distinct syntaxes---one for input, one
for memory and reasoning, and one for display.

NFLT-expressions that are in some way associated with potentially useful
information are presently stored in a discrimination net that maintains a
unique, canonical version of each compound concept and proposition in the
ANALYST's explicit memory.  An NFLT-expression is located in the
discrimination net by computing for it a unique list of indexing keys.
The first element of this key-list is a concept-construction operator
that specifies one way in which the embodied concept may be constructed
from component concepts.  The remaining members of the key-list are the
component concepts, either atomic or compound.  Each logically-compound
component concept is itself indexed in the discrimination net by its own
key-list, consisting of a concept-construction operator and component
concepts.  Thus the discrimination net implicitly records for each stored
compound concept a complete analysis into {\sl atomic} component concepts.
Quite apart from its role in the indexing scheme, this conceptual analysis is
of theoretical significance as a demonstration of the compositional semantics
of NFLT.

\ni 3. A matcher for NFLT was designed and partially implemented.  It is a
unifier and was implemented by writing a matcher-generator and applying
that generator to a description of the NFLT data-structure.  This
matcher-generator is a major result since it allows one to abstractly
describe pattern and datum data structures and to automatically generate a
unifying pattern matcher on those data structures.  A significant feature
of the class of matchers that the matcher-generator produces is that they
unify `star-variables.'  Star-variables match $0$ or more elements in a
single-level stream of elements.  The Gabriel reasoner (described below)
uses a tree-structure unifier which was the model for the
matcher-generator.  Recent work on the tree-structure unifier needs to be
incorporated into the matcher-generator and hence the NFLT matcher.
Recent insights concerning the use of subformulas of quantified NFLT
expressions as patterns also need to be taken into account.

\ni 4. Epistemological work was done on a scheme for causal reasoning that
will offer new solutions to the frame and qualification problems.  This
work is presently being completed and implemented in the ATREAS commonsense
reasoner described in item 7 below.

\ni 5. Detailed epistemological studies were made of some of the
commonsense factual reasoning involved in plan production and of the
interaction of this reasoning with the planning process.  This reasoning
was found to be quite complex.  As an example of some of the relevant
knowledge that we have formalized in these studies, we present one of the
commonsense causal laws that our reasoner is currently being developed to
utilize (Law of Causal Influence for Driving):

Here is a rough statement in English of the law:  ``If a person
tries to drive a car from location $L↓1$ to location $L↓2$ via drive-path
V, leaving at $T↓1$ and arriving by $T↓2$, then, provided that the car is
located at $L↓1$ at time $T↓1$, and that there is sufficient time for the
intended driving, and provided that certain further conditions are met
concerning the condition of the car, drive-path, and person, this will
tend to cause the person to succeed in his attempted driving.''

The following is a computer-readable formalized version of the law (NFLT
Lisp-form input syntax):

\bcode
((ALL P PERSON
      X AUTOMOBILE
     $\up$X (CONCEPT $\up$X (OF X))
     L1 LOCATION
    $\up$L1 (CONCEPT $\up$L1 (OF L1))
     L2 LOCATION
    $\up$L2 (CONCEPT $\up$L2 (OF L2))
      V (DRIVE-PATH V L1 L2)
     $\up$V (CONCEPT $\up$V (OF V))
     T1 TIME
    $\up$T1 (CONCEPT $\up$T1 (OF T1))
     T2 TIME
    $\up$T2 (CONCEPT $\up$T2 (OF T2)) )
 (TENDS-TO-CAUSE
    (AND (LOCATED-AT X L1 (ATT T1))
         (GREATER (!TIME-DIFFERENCE T1 T2) (!DRIVE-TIME L1 L2 V))
         (TRY P ($\up$(DRIVE I (VEHICLE ($\down$ $\up$X))
                           (FROM ($\down$ $\up$L1))
                           (TO ($\down$ $\up$L2))
                           (VIA ($\down$ $\up$V))
                           (LEAVING-AT ($\down$ $\up$T1))
                           (ARRIVING-BY ($\down$ $\up$T2)) ) )
                (WHILE (AND (RUN-OK X)
                            (DRIVABLE V)
                            (PHYSICALLY-ABLE P DRIVE)
                            (KNOW-HOW P $\up$DRIVE)
                            (EFFECTIVELY-IDENTIFIABLE 
                               P ($\up$(($λ$ P X L1 L2 V T1 T2)
                                    (DRIVE P (VEHICLE X)
                                             (FROM L1)
                                             (TO L2)
                                             (VIA V)
                                             (LEAVING-AT T1)
                                             (ARRIVING-BY T2) ) ))
                                 (C1 $\up$I) (C2 $\up$X) (C3 $\up$L1) (C4 $\up$L2)
                                 (C5 $\up$V) (C6 $\up$T1) (C7 $\up$T2) ) ))
                (START-TIME T1) 
                (STOPPING-ONLY-FOR-STRONG-REASONS) ) )
    (DRIVE P (VEHICLE X)
             (FROM L1)
             (TO L2)
             (VIA V)
             (LEAVING-AT T1)
             (ARRIVING-BY T2) )
    (STRENGTH SUFFICIENT-IF-UNPREVENTED) ) )
\ecode

\ni 6. A storage manager for ANALYST has been implemented and tested.  However,
it is not presently being used because the space problems it would help to
alleviate have not yet arisen in our prototype implementations.

\ni 7. Two prototype commonsense-reasoning modules for the ANALYST were implemented
and tested.  One was written by Richard Gabriel and is used to explore modes of
reasoning, methods of evidence gathering, and efficiency issues in searching for
information.  The second reasoner, written by Lewis Creary, is partially based
on the first, but utilizes a more complex representation language (NFLT) and
reasoning graph, and a redesigned reasoning algorithm.  Gabriel's reasoner
is used for rapid experimentation with ideas, while the final ANALYST module
will descend from Creary's reasoner.  Results of the most successful
experiments with the former will be incorporated into the latter.

A pervasive and fundamental characteristic of commonsense factual reasoning is
the weighing of all reasonably discoverable relevant considerations before
drawing a conclusion.  The main structural components of a simple commonsense
factual inference are a target proposition (the conclusion or its negation)
and a number of separate {\sl considerations} (i.e., sub-arguments) that
bear evidentially on this proposition.  The various considerations bearing on
a single target proposition may differ in {\sl directional tendency}
(confirmation or disconfirmation), in {\sl inherent relative strength},
and in {\sl force} (i.e., absolute strength {\sl in situ}).  Values on
the first two of these attributes for a given consideration depend only on the
nature of the consideration, whereas the {\sl force} of a consideration in
a particular application depends also on how well its premises are known.

Both of our commonsense reasoning programs attempt to find and evaluate
all reasonably discoverable considerations bearing on the truth of a given
statement.  Gabriel's REASON program currently handles 19 specific types
of consideration.  Among the types with maximal inherent relative strength
are those corresponding to rules of deductive logic, such as tautological
considerations (supporting statements true because of their logical form),
Boolean considerations (for example, $\hbox{A}∧\hbox{B}$ is true if A and B are
true), modus ponens considerations (B is true if A and
$\hbox{A}⊃\hbox{B}$ are true), identity considerations
($\hbox{P}(\hbox{a})$ is true if $\hbox{b}=\hbox{a}$ and
$\hbox{P}(\hbox{b})$ are true), and quantificational considerations
($\hbox{P}(\hbox{a})$ is true if $∀x.\hbox{P}(x)$ is true).  Rewrite rules
are included as reasoning experts to obtain the force of standard logical
deductions. For instance $¬¬\hbox{S}$ is equivalent to S and
$¬∀x.¬\hbox{P}(x)$ is equivalent to $∀x.\hbox{P}(x)$.  There are 9 such
reasoning experts.

Among the consideration-types with less-than-maximal inherent relative
strength is the {\sl statistical} consideration, depending on a premise
containing a statistical quantifier, such as `GREAT-MAJORITY.'  When the
truth of $\hbox{can-fly}(\hbox{tweety})$ is supported by the statements
$\hbox{bird}(\hbox{tweety})$ and
$((\hbox{GREAT-MAJORITY\ }\hbox{x\ }\hbox{bird})\hbox{can-fly}(\hbox{x}))$,
the support is less strong than it would be if `GREAT-MAJORITY' were replaced
by `ALL.'  Stated another way, if one knows with certainty that Tweety is a
bird and that the great majority of birds can fly, then, provided that this
knowledge is not preempted by other statistical knowledge one has about
Tweety, it gives rise to a statistical consideration in support of the
statement that Tweety can fly.  While this consideration is genuine, it
provides no certainty that Tweety can fly.  On the other hand, if one knows
with certainty that that Tweety is a bird and that {\sl all} birds can fly,
then there exists a deductive consideration conferring certainty on the
conclusion that Tweety can fly.

There are other non-deductive consideration-types handled by Gabriel's
program, but they are presently subject to debate and possible revision.

\eat

Other non-deductive consideration-types (in addition to the statistical)
handled by Gabriel's reasoner are in a class of interesting
consideration-types which results from the observation that $P(a)$ may not
be the case, but perhaps $∃x.x=a∧P(x)$. This mode of reasoning can
continue with $∃y.∃x.y=x∧a=x∧P(y)$. Since this line of reasoning leads the
program to try to enumerate all of the individuals that it knows about,
cutting off the search at some point and reasoning about the extent of the
list collected so far must be performed if any conclusion is to be made.
For example, if a particular penguin is known, and if it is known that
this particular penguin is the only possible candidate penguin that could
be identified as Tweety, then it is only necessary to look to that penguin
in the search to make a strong case that if Tweety is not this particular
penguin, that Tweety is not, then, a penguin, and that Tweety can fly.

This mode of reasoning is similar to one that Allan Collins
suggested. That mode allowed one to state that if some fact were true,
then it would be important enough to be known.

Two reasoning experts are currently included in this class, along with an
expert to control combinatorial explosion during the search process.

A further embellishment on this mode of reasoning concerns the names
that are given to individuals. For instance, Tweety is represented
to the reasoning program as a data structure---a memory node of sorts---which
includes a name as part. Thus it is explicitly stated that the name of
the individual represented by the node corresponding to Tweety is `Tweety.'
There is a reasoning expert that infers that most individuals with different
names are distinct.

\endeat

The consideration-gathering process consists of building what was originally
conceived as a tree of dependencies, where the daughters of a node represent
the considerations that bear on that node.  The original tree-building process
was such that it was possible for two distinct nodes in the tree to have the
same content (with different links).  However, it was found experimentally
that if care is not taken to avoid such a duplication of node-contents,
serious inefficiencies in searching can arise.  For this reason, the
consideration-dependency-network is now a graph that is usually not 
a tree, with each node having a unique content.  A node in this graph is a
content-triple comprising a target proposition, a reasoning expert, and a
reasoning context, together with various links and pointers.  The uniqueness
of node-contents has been preserved (but with a changed notion of content) in
Creary's reasoner.

Creary's ATREAS commonsense-reasoning module for the ANALYST utilizes the
new representation-language, NFLT, and a very general reasoning graph capable
of supporting both forward and backward factual reasoning.  The reasoning
graph is the main data structure used by the commonsense reasoner and
consists of complex propositional nodes connected by complex labelled links
representing considerations (i.e., logical sub-arguments both for and against
various target propositions).  Commonsense reasoning begins with a specific
goal---to evaluate the epistemic status of a particular (usually small) set of
target propositions.  This goal, together with a certain allotment of
information-processing effort that may be expended on it, arises within some
larger problem-solving context involving factual inquiry, planning,
deliberation, or the like.  A goal-directed, heuristically-guided search is
conducted for considerations both for and against the target propositions.
This search may give rise to new target propositions, for which considerations
are also sought, in their turn.  The consideration-search terminates when
either it runs out of target propositions or the allotted effort (currently
in arbitrary units) has been expended.  Finally all the considerations
discovered are evaluated and composed and a conclusion is drawn, if
warranted.

The search for considerations is directed by specialized reasoning experts.
In a full bi-directional implementation there will exist both a forward and a
backward reasoning expert for each rule of evidence.  At present only a few
of the backward reasoning experts have been implemented.  Currently under active
development are more reasoning experts (both deductive and non-deductive) and
heuristic knowledge for guidance of the consideration-search.

There is presently on-line at SAIL a small demonstration version of the ATREAS
system, which can be run in order to get a feel for the general character of
the reasoning program, the major data structures that it uses, its supporting
interactive environment, and the NFLT representation language.  The premises
available for the demonstration include information about birds and penguins
in general, and about a particular penguin named `Slick.'  Given only that
Slick is a bird, that the great majority of birds can fly, and that no
penguins can fly, the program concludes it is very likely that Slick can fly.
However, if we add to these same premises the further information that Slick
is a penguin, the program will then conclude it is most {\sl un}likely
that Slick can fly.  This demonstration illustrates what is now widely
referred to as the `non-monotonicity' of commonsense reasoning: the fact
that the mere addition of new premises can invalidate a previously reached
conclusion---something that cannot happen in purely deductive reasoning.

The theoretical model of commonsense reasoning on which this reasoning program
is based is discussed in a forthcoming technical report \ref:Creary.1983..

\ni 8. A substantial interactive research environment for Creary's
commonsense reasoner was implemented, tested, and documented on-line.  It
consists of an interactive program control and four co-routined
sub-programs for exercise of the reasoner and examination of data
structures.  These sub-programs are as follows:

\numitem{a.}EXERCISE-COMMONSENSE-REASONER  (permits convenient interactive
exercise of the commonsense reasoning program).

\numitem{b.}EXPLORE-TASK-RECORD  (permits convenient interactive examination of
a previously executed agenda of reasoning tasks).

\numitem{c.}EXPLORE-REASONING-GRAPH  (permits convenient interactive examination
of reasoning graphs produced by the commonsense reasoner).  An important and
particularly useful feature of this sub-program is its ability to provide
concise, easily readable summaries of all the considerations found by ATREAS
during the reasoning process.

\numitem{d.}EXPLORE-DISCRIMINATION-NET  (permits convenient interactive
examination of a discrimination net that uniquely indexes logically compound
concepts and propositions).

These programs relieve much of the tedium that would otherwise be involved in
experimenting with the ATREAS reasoner and permit efficient high-level
debugging of inference rules and factual information.  The programs presently
have a combined repertoire of 58 high-level commands, each one requiring 2 or
3 keystrokes for the command mnemonic, and (typically) from 0 to 3 arguments.
These programs are largely self-documenting through the use of
help-commands that offer information at three different levels of detail.

\ssect Implementation Statistics.

The programs described in items 7 and 8 above presently comprise over 10,000
lines (excluding blanks) of sparsely commented (but fairly readable) MacLisp
code.  This breaks down roughly as follows:

$$\vcenter{\halign to size{\hfill#\tabskip 0pt plus 2pt
⊗#\hfill\tabskip 0pt\cr
2700 lines:⊗REASON commonsense reasoner  (Gabriel)\cr
200 lines:⊗Tautology checker (Gabriel)\cr
1400 lines:⊗ATREAS commonsense reasoner  (Creary)\cr
600 lines:⊗Context mechanism shared by both reasoners  (Gabriel)\cr
2400 lines:⊗Interactive research environment for ATREAS/NFLT  (Creary)\cr
2800 lines:⊗NFLT: programs for translation, display, logical analysis,\cr
{}⊗and uniquifying formula storage.  (Creary)\cr
400 lines:⊗Conceptual structures for ATREAS/NFLT  (Creary)\cr}}$$

These are the programs that we are currently using on a regular basis in our
experimentation and development work.

\sect Formalisms for Reasoning about Programs.

Carolyn Talcott is studying formal systems and structures for representing
and proving properties of programs, including
computations, programming systems, and programming environments.

One objective is to account for and elucidate programming practices common
in the Artificial Intelligence community.  This includes studying the
kinds of programs and structures used both in building systems for
representing knowledge, reasoning, and planning, and in building systems
for building systems.

An important aspect of the AI style of programming is the use of programs
and other complex structures in a variety of ways.  Some examples are:

\ni 1. Using programs to compute (partial) functions.  This is the `obvious'
use of programs. The important point is that the data structures these
programs use often represent complex objects of the sort not usually
treated in work on program verification or specification.

\ni 2. Using programs as functional arguments.
For example, a mapping function takes a function and a structure
as arguments and produces a new structure by applying the given 
function to each component of the input structure.
Search routines are often parameterized by functions for
generating successor nodes or by functions for evaluating positions.

\ni 3. Using programs as functional values.  Specifying some of the
arguments of a function and then `partially' applying that function
produces a second function as a value.  The function
$λ(\hbox{x},\hbox{y})\hbox{x}+\hbox{y}$, when
supplied with the argument 7 for the parameter y, yields the function
$λ(\hbox{x})\hbox{x}+7$, which adds 7 to its
argument.  Combinators applied to functions return functions as values.
For example $\hbox{compose}(\hbox{f},\hbox{g})(\hbox{x}) =
\hbox{f}(\hbox{g}(\hbox{x}))$ and
$\hbox{subs}(\hbox{f},\hbox{g})(\hbox{x}) =
(\hbox{f}(\hbox{x}))(\hbox{g}(\hbox{x}))$.

\ni 4. Using programs to represent procedural information.
Information in data bases, knowledge, and problem solving strategies
may be represented procedurally (as a program).

\ni 5. Using programs to represent infinite or partially completed objects
such as streams, sets, or continuations.  Suppose there are many solutions
to a given problem. One means of representing the solutions is by a program
which, when queried, produces a solution and another program representing
the remaining solutions.

\ni 6. Using programs as functions that specify control structure.
Co-routines (co-operating processes) can be expressed using functions as
can many forms of delayed evaluation.  For example $λ()\hbox{f}(\hbox{x})$
represents f applied to x, but will only be evaluated if explicitly called
for (by application to an empty list of arguments).

\ni 7. Using programs as `actors' and as behavioral descriptions of complex
data structures. That is, instead of implementing a data structure as
a block of storage along with a set of programs for manipulating that
storage, one can write a program which takes manipulation names
and values as arguments and which updates its internal environment
to achieve the effect of the desired data structure, perhaps returning a 
program representing the updated data structure as a value.

\ni 8. Using programs as objects that can be constructed, transformed,
interpreted, and compiled.  We include here definition of data structures,
compiling, and program synthesis.

Other aspects of this style of programming include non-local control
mechanisms such as catch and throw, macros and metafunctions (for example,
to define new constructs or implement convenient abbreviations), `hooks'
into the underlying system (hooks provide dynamic access to the symbol
table and other data structures used by the interpreter and other system
routines), and use (often interchangeably) of both compiled and
interpreted code.

\ssect Goals and applications.

Our goal is to be able to treat the diverse uses of programs in an
integrated system.

We want to develop informal and formal methods to express and prove
properties that reflect naturally the intent of system designers and
programmers.  The informal part is based on a model of computation
(computation structure) that naturally accounts for the various styles of
programming encountered in AI systems.  There are two ways to mechanize
this model.  One is to encode the structure as data.  The second is to
define a formal theory for proving assertions about the structure.  The
connection between the two provides additional means of expressing
properties of the system.

Although the initial work will be abstract and technical, there
are many practical applications.  Some of these are summarized
below along with some important extensions.

\ni 1. Mechanization of the system via formalization of the metatheory and
model theory will provide an implementation of the system and a basis for
mechanical proof checking.  It also will provide tools for building
systems---by providing data types corresponding to some of the complex
structure used in these systems.

2. We will be able to prove properties of `real' Lisp programs, such as
programs that contain arbitrary assignments, non-local control such as
CATCH and THROW, as well as programs containing MACROs and META functions.
We will also treat programs that act on memory structures---such programs
in Lisp use operations that are destructive on list structure, such as
RPLACA and RPLACD.

\ni 3. Abstract data structures (domains and operations) will be formulated in
a natural manner within the proposed system.  Thus it will be used as a
framework for understanding data abstraction and, in particular, for
analyzing the notion of parameterized data type, which has been the subject
of recent investigation from several points of view.  See, for example,
\ref:Thatcher.1979. and \ref:Cartwright.1980..

\ni 4. We will formalize the notion of a computation system as computation
theory plus implementation.  Here we move from the static aspects of a
computation theory to the dynamic aspects of interactive systems.  An
interactive and dynamically changing system will be explained in terms of a
theory, a model, and an interpretation (dynamically) connecting the two.

\ni 5.  Formalization of the dynamic aspects of a programming system will
provide a framework for talking about declarations and definitions,
debugging, handling ERROR conditions, and distinguishing between different
kinds of undefinedness---abnormal termination versus non-termination.  A
clean, simple description of a system makes provision for and use of debugging
facilities easier, more straight-forward, and more effective.

\ni 6. We will be able to develop a model and implementation for logic
programs.  Easily identified, mathematically smooth subsets of the
computation theory can be interpreted as a model for logic programs.  Our
constructions are uniformly paramaterized by the data domains on which
computation is being defined.  This makes the connection with logic
programs ($\hbox{logic} (=\hbox{data})+\hbox{control} (=\hbox{PFN})$)
natural. A `PFN' is a computational equivalent to a partial function.

\ni 7. Ideas for expressing properties of high-level program descriptions
are useful for compiling and automatic program optimizations.

\ssect Understanding programming systems.

The sort of programming system we wish to study is a full interactive
Lisp-like system including language, interpreter, compiler, and debugger.
Our approach to understanding such a system---for instance, to be able to
make precise statements about its behavior, semantics, and extensions---is
to begin with a model of computation (computation structure) that reflects
the computational aspects of the system.  We then consider encodings of
this model in suitable data domains.

Within our model the semantics of a programming language can be expressed
in a number of ways, for example as the function computed by an
applicative program or by using structures representing the computation
defined by a program.  The connections between a program, the function it
computes, and the computation it defines can be made precise.  The
different views of programs (a) as functions---which may take functions as
arguments and return functions as values---and (b) as data can be
mechanized.  This is crucial for applications of the theory to other areas
of reasoning such as building models or plans.

\ssect Construction of computation structures.

A computation structure contains data, PFN's, a means of evaluating
expressions, a means of applying PFN's to arguments, and notions of
subcomputation.  Computation structures are constructed uniformly from
data structures---a collection of data and operations taken to be
primitive.  There is a natural domain of values extending the basic data
domain and including all PFN's as values.  Applicative, imperative,
iterative, recursive, and many other styles of programming are naturally
expressible as PFN's.

We begin with a data structure---the collection of data and operations
taken to be primitive---and construct from it a computation structure. 
Computation is defined using conditional expressions, abstraction, application,
environments, and closures. There is a natural domain of values extending
the basic data domain and including all PFN's as values.
Applicative, imperative, iterative, recursive, and many other styles of
programming are naturally expressible as PFN's.
Computation structures are uniformly parameterized by data structures
in the sense that the constructions define an effective mapping from
data structures to computation structures.

Two notions of computation are distinguished, which are called
`computation over a data structure' and `computation over a memory
structure.'  Computations over data structures use only the primitive
operations that construct and examine data; for example, in pure Lisp
they are CAR, CDR, CONS, EQUAL, and ATOM.  Computations over memory structure
use, in addition, destructive primitive operations, such as RPLAC's and
array assignments.  The same basic language serves to define either form
of computation.

Our notion of computation theory draws on ideas of an equation calculus
\ref:Kleene.1952. \ref:McCarthy.1963., hereditarily consistent functionals 
\ref:Platek.1966., abstract recursion theory \ref:Moschovakis.1969.
\ref:Fenstad.1980., and
primitive recursive functionals \ref:G\"odel.1958.. The resulting programming
system is related to SCHEME \ref:Steele.1975..

\ssect Multiple arguments and values.


In a computation structure PFN's are applied to a single argument which is
a `cart' of objects.  The result of applying a PFN, when defined, is a
cart of values.  Carts are like lists, but in a computation the list is
not constructed---virtual lists.  They provide a natural means of
expressing computations with multiple arguments and multiple values.  The
use of carts suggests a natural extension to the usual methods for
algebraic specification of data types.  It also suggests an interesting
class of (rational) operations on data domains.

\ssect Subsystems.

A useful technique for reasoning about programs is to identify natural
subclasses of PFN's and to formulate natural embeddings
among the classes where appropriate.  Specification of properties and
reasoning can then be carried out in the corresponding limited domain.

In our basic model many useful classes arise naturally from purely
`syntactic' considerations.  These include purely applicative,
simple imperative (loops with assignment limited to local
context), mixed imperative and applicative, and iterative.

There are also notions of `shape' and of `well-shaped' PFN's and
computations that seem to be useful for identifying interesting classes of
PFN's.  Shape is an intensional---essentially syntactic---analog to the
logical notion of type. Logical types are sets constructed from base sets
using constructions like cartesian product and exponential (function-space
formation).  See \ref:Scott.1975., \ref:Feferman.1977., or \ref:Feferman.1981..
Shape is related to notions of type or functionality used in combinatory
logic \ref:Hindley.1969. and \ref:Coppo.1980..
Shape is also related to notions of type used by programming and proof
systems that allow parameterized types \ref:Milner.1978..

Certain properties and principles hold for a PFN by virtue of 
its being well-shaped, and this can be used to simplify and guide proofs.
It can also be useful in the design of programs and for expressing
properties that may be of use to a compiler.

Another way of identifying interesting classes is to embed one computation
structure in another.  For example, to take advantage of methods developed
in temporal logic one would embed a temporal model of computation and
apply the temporal methods to the resulting subsystem.

\ssect Computations and programs as data.

The mechanization (formal encoding) of a computation structure turns PFN's
and computations into data allowing us to speak of operations on PFN's and
on computations.  In addition to being able to represent operations, we
can discuss properties of these operations.  Some properties of interest
are:

\numitem{i.}Soundness---preserving the function computed;

\numitem{ii.}Effect of an operation on the properties of the computation defined by a 
         program.  Properties of interest include
         recursion depth, memory usage, and other measures of execution cost;

\numitem{iii.}Program size.


The traditional kinds of operations on programs include transformations,
translations and program construction.  

A further kind of operation on programs is the construction of derived
programs; this is based on an idea of McCarthy.  Derived programs compute
properties of the original program.  Complexity measures can be expressed
via derived programs.  For example, depth of recursion, number of CONSes
executed, or number of subroutine calls are typical complexity measures
for Lisp.  Properties of the these derived programs are similar to
properties treated in the traditional work in analysis of algorithms.
Many other properties of a program can be computed by derived programs.
Some examples are structures representing traces or complete computation
trees and other structures useful for debugging.

\ssect Notions of equivalence on computation structures.

When programs are used in the different contexts and with the variety 
of interpretations discussed above, questions such as correctness of 
program transformations become complex.  In order specify the intent 
and correctness of programs and operations on programs we must be able 
to express the precise sense in which programs are to be considered equivalent. 
The classical (extensional) notion is that PFN's are equivalent if 
they are defined on the same domain and have the same value on all arguments
in the domain of definition.  When arguments and values can be PFN's this 
is not an adequate definition.
Notions of equivalence are also important simply to express the fact that
different programs define the same computations or have the same
behavior.

\ssect Criteria for an adequate formal system for reasoning about PFN's.

In an adequate formal system definitions and assertions as well as
reasoning about computation structures should be naturally and efficiently
expressed.  This implies a number of criteria for such a system.

\ni 1. Data and PFN's should be part of the domain of discourse.  PFN's should
behave, in some respects, as functions.  They should also be able to be
arguments to and values of PFN's.  The collection of PFN's that can be
proved to exist should be closed under the usual constructions on
computable functions. These constructions include conditionalization,
abstraction, application, composition, closure, iteration (corresponding
to loop programs), and recursion.  Combinatory operations on PFN's should
be representable---as PFN's.  There should be principles for introducing
schemata for proving properties of special classes of PFN's.

\ni 2. There should be a means of introducing domains (sets) and operations
on domains including boolean operations, cartesian product, and formation of
finite sequences or trees.  Limited principles of inductive definition
together with the corresponding principles for proof by induction are also
needed.  Domains may contain data, PFN's, or both.

\ni 3. The system should be `parameterized' by the intended computation
domain (the primitive data types and operations).  This reflects the
principle of separation of control and data which is important for
modularity and stability of a computation system.

There have been many systems developed by logicians for formalizing
various kinds of mathematics including constructive analysis, constructive
algebra, and logic.  Many of the results can be easily modified to apply
to reasoning about programs.  Of particular interest is the work of
\ref:Feferman.1974., \ref:Feferman.1978., and \ref:Feferman.1981. on formal
systems for constructive and explicit mathematics (analysis).  Other
relevant work includes \ref:Beeson.1980., \ref:Martin-L\"of.1979.,
\ref:Nordstr\"om.1981., \ref:Scott.1977., and \ref:Tennant.1975..

\sect Accomplishments.

\ni 1. The definition of the applicative fragment of the computation structure
(called RUM) has been completed.  This includes the associated notions of
evaluation of expressions, application of PFN's, and the subcomputation
relation.

\ni 2. A variety of simple examples have been worked out in RUM.  These include:

\numitem{i.}representation of numbers and number-theoretic functions.

\numitem{ii.}definition of several combinators---as examples of the
expressiveness of both PFN's and of multiple arguments and values.

\numitem{iii.}computing with streams/continuations---statement and proof of
correctness of a simple pattern matcher using continuations to do
backtracking.  The pattern matcher produces a stream of matches.

\numitem{iv.}representation of tree-like structures using PFN's.

\numitem{v.}representation of re-entrant (circular) memory structures using PFN's.
These are essentially the structures implicit in PROLOG when `occur check'
is omitted from unification.  Using PFN's, structures corresponding to
solutions of sets of equations can be represented, but it seems that
destructive operations are not representable as (extensional) operations
on PFN's.

Detailed proofs of properties of the structures and PFN's defined were given.

\ni 3. RUM was extended to include CATCH and THROW (non-local control)
constructs.  Example proofs of properties of PFN's using these constructs
were worked out.  A computation-preserving map from the extended RUM to the
original was defined---CATCH elimination.  

\ni 4. We defined a class of PFN's called iterative PFN's which extends the
usual `first order' notion of (flowchart) programs \ref:Manna.1978..  We
generalized the invariant assertion, intermittent assertion, and subgoal
assertion methods of verification to this class of PFN's.  We proved the
Manna formulae \ref:Manna.1969. for partial and total correctness in this 
setting and also the equivalence of his total correctness formula to the 
intermittent assertions formula.

\ni 5. A Computation Induction scheme for recursively defined PFN's was defined
and used in many of the examples.

\ni 6. A paper describing the above work is in preparation.

\ni 7. Some progress has been made towards a formal theory.  Much work remains
to be done.

\sect EKL.

Jussi Ketonen and Joseph Weening have been working on further development of
EKL, an interactive proof checker in high-order predicate calculus.

The emphasis has been on creating a system and a language that would
allow the expression and verification of mathematical facts in a direct
and natural way. The approach taken has been quite successful: Ketonen has
been able to produce an elegant and eminently readable proof of Ramsey's
theorem in under 100 lines. At the same time EKL is versatile enough to be
able to verify the associativity if the Lisp APPEND function in just one
line.

The above results are important in that they indicate that programs
previously thought to be too complex for mechanical verification are now
within the reach of sufficiently powerful proof-checking systems.

\ssect Accomplishments.

\ni 1. A manual reflecting the state of EKL during December 1982 was written
by Weening and Ketonen.

\ni 2. EKL has been tested by its use in CS206, a course on Lisp programming
at Stanford. As homework assignments, students used it to prove facts
about Lisp programs.

\ni 3. One of the outgrowths of this development work has been a formalisation
of the underlying logic of EKL.  EKL was based on a high-order predicate
logic since we felt that it is important to be able to discuss functionals
and lambda-abstraction in a natural way.  At the same time it seemed to us
that the currently fashionable formalisations of high-order logic were
still inadequate for expressing mathematical facts. Our approach was to
gradually modify the logic of EKL to accomodate intuitively
straightforward extensions without worrying too much about the formal
underpinnings.  It is satisfying to note that we have now come full
circle:  Ketonen has shown that the logic of EKL can be formally expressed
(along with its consistency proofs, etc.) in a very elegant and precise
way---in fact, in a more elegant way than the logics we started out with.
This theory also embodies the way EKL can talk about meta-theoretic
entities---to our knowledge it is one of the first instances of a logical theory
of mathematics that can discuss denotations in a coherent way.  Ketonen
and Weening are in the process of writing a paper on this.  A large amount
of effort has been spent on the EKL rewriting system---currently the most
powerful and versatile component of EKL.  Ketonen has come up with a new
architecture for rewriting systems that is quite different from the ones
currently used, say, by Boyer and Moore.  Accompanying the rewriter there
is also a notion of a language for rewriting---how to control the process
through simple instructions to EKL.  This has turned out to be a fairly
powerful tool in reducing the lengths of proofs in EKL.

\ni 4. A decision procedure for an important fragment of the `obvious' theorems
of first order logic was designed and implemented.

\sect Lisp Performance Evaluation.

Richard Gabriel is studying the issue of performance evaluation of Lisp
systems, both in general by studying the ingredients of performance
of a Lisp implementation and in particular by benchmarking a number
of important existing Lisp implementations.

\ssect Accomplishments.

\ni 1. 19 Lisp benchmarks were designed. At the Lisp and Functional
Programming Conference, the attendees interested in performance evaluation
stated that they would prefer to see Richard Gabriel do all of the
benchmarking personally.  Therefore, he is currently benchmarking those
implementations most often inquired about. These are the Xerox D series
(Dolphin, Dorado, and Dandelion), the Symbolics LM-2 and 3600, Vax Lisps
(Franz, DEC/CMU Common Lisp, InterLisp-Vax, NIL, and PSL), MC68000-based
Lisps (Apollo running PSL, SUN running PSL and Franz, and HP-9836 running
PSL), and DEC-10/20 Lisps (MacLisp, InterLisp-10, and Elisp).

\ni 2. One benchmark has been run on all of the various Lisp configurations, and
there are 75 measurements. These results have been made available to several
ARPA contractors to aid hardware acquisition decisions.

\ni 3. A paper, ``Performance of Lisp Systems,'' has been written (with Larry
Masinter of Xerox PARC) and published in the proceedings of the ACM
Symposium on Lisp and Functional Programming; this paper discusses the
methodological issues for performance evaluation and presents some of the
results mentioned in 1.  This paper will be part of the final report
delivered in December 1983. 

\ni 4. Some qualitative statements on the Lisp systems in the study have been
gathered for the final report. These are facts about the Lisp systems that are
of interest in comparing implementations and which are not performance-centered.

\ni 5. A detailed analysis of the DEC/CMU Vax Common Lisp has been completed by
Richard Gabriel and Martin Griss (from the University of Utah). This analysis
is being prepared for publication.

\sect Common Lisp.

Both Richard Gabriel and John McCarthy have been active in the
development and design of Common Lisp.
Common Lisp is the combined effort of eight different Lisp implementation
groups aimed at producing a common dialect of Lisp while allowing each
group to exploit its own hardware.  These groups are: Spice Lisp at CMU,
DEC Common Lisp on Vax at CMU, DEC Common Lisp on DEC-20 at Rutgers, S-1
Lisp at LLNL, Symbolics Common Lisp, LMI Common Lisp, Portable Standard
Lisp at Utah, and Vax NIL.  Common Lisp is a set of documents, a language
design, and a common body of code.

The main goal of Common Lisp is to unify the experiences of the
Lisp implementations that are descended, either historically or
philosophically, from MacLisp. MacLisp is a dialect of Lisp that
emphasizes ease of system-building and efficient execution of numeric
code.  

Other goals of Common Lisp are to provide a workbench programming
language for artificial intelligence, symbolic algebra, robotics,
and education for the next decade. With such a commonly available
and commonly used Lisp it would be possible for researchers to
exchange programs with a minimum of effort, even though the host
computers could be very different. Such a Lisp would be powerful enough
to write a sophisticated operating system sufficient to support its
own use and would, thereby, prove to be a useful systems research tool
as well as a tool for creating Lisp machine environments.

With a powerful Lisp widely available, research centers might not have
to consider the language features of the Lisp(s) available on various
computers as part of the decision regarding what hardware to purchase.
In this way a more intelligent and effective choice could be made.

Common Lisp should support an easily-understood, portable programming style.
By making a large number of packages written in Lisp available it is hoped 
that not only would the amount of work needed to get a system running be
low, but the overall programming style and methodology would be improved
through exposure to the code written by expert programmers.

\ssect History.

After the usefulness of the PDP-10 as a Lisp engine declined because its
address space was limited to 18 bits, several implementation groups
started to implement Lisps for computers with larger address spaces, and
these implementors tried to improve and extend MacLisp, both to take
advantage of lessons learned from MacLisp and the various languages built
on top of it (Scheme, for example) and to also exploit the architectures
the implementors were using.

It soon became clear to several of the implementors (Richard Gabriel of
Stanford and Lawrence Livermore National Laboratory, Guy L. Steele Jr. of
Carnegie-Mellon University, Jon L. White then of the Massachusetts
Institute of Technology, and Scott Fahlman of Carnegie-Mellon University)
that the situation of four different Lisps---Vax NIL, SPICE Lisp, Lisp
Machine Lisp, and Franz Lisp---all descended from MacLisp, all used by
ARPA-sponsored institutions, and each different from the others in subtle,
yet important, ways, was intolerable to the research community. Several
key meetings among the implementors resulted in an initial commitment to
unify the approaches in the form of a large, common subset, which was to
be called `Common Lisp.' Of the four major Lisp implementations, only
Franz Lisp did not appear interested in joining the Common Lisp group, and
for financial rather than philosophical reasons.

Since this informal group got together, the language, Common Lisp,
has been largely designed and a manual written that describes the
language at user-level.  The original informal group has expanded into a
larger, formal committee which is collaborating on the language design and
documentation in a loose fashion. This group, called the `Common Lisp
Group', maintains a mailing list and an archive of working messages at
SAIL (Stanford Artificial Intelligence Laboratory).
Many decisions have been made about the political organization of Common
Lisp and about what the manual does and does not require of an
implementation.

To be most useful, Common Lisp must support a large body of packages and
routines, so that a tradition of code, so to speak, is maintained. For
example, pattern matchers, object-oriented programming packages, and
indexing routines should be available so that projects requiring these
tools can use existing, well-tested code. In addition, these packages
ought to be of certified quality of functionality and documentation.

If Common Lisp is to be widely used it must be available on hardware not
currently supporting Common Lisp dialects. Since Common Lisp is a large
language, producing a working Common Lisp simply from the manual would
require several man-years of effort. One of the next tasks to be
undertaken is to define Common Lisp in terms of a {\sl virtual machine}
description.

Such a description is a formal definition of a number of primitives that
must be defined on the hardware in question. Then the remainder of Common
Lisp is defined as a body of Common Lisp code written with the assumption
that these primitives exist. Once these primitives are defined on a piece
of hardware, a Common Lisp interpreter is gained by `loading' the body of
Common Lisp code.

\ssect Compilers.

Richard Gabriel has been working on compilers for Common Lisp, targetting
high-performance, stock-hardware computers---in this case the S-1 Mark IIA
supercomputer \ref:Brooks.1982a. \ref:Brooks.1982b. \ref:Brooks.1983..
Discussion with Prof. Martin Griss from the University of Utah on the
topic of portable compilers has led to interest in a joint
high-performance portable compiler project for Common Lisp between Stanford
and Utah.

It it hoped that this compiler would be targettable both to medium-performance
computers, such as those based on MC68000 microprocessors, and to high-performance
multi-processors, such as the S-1 Mark IIA.

\sect Automatic Construction of Special-purpose Programs.

Chris Goad has been working on the automatic construction of
special-purpose programs.  In software development the aims of efficiency
and generality are often in conflict.  It is common that specialized
programs, which take into account complex details of the situation in
which they are used, can be made much faster than cleaner, more general
programs. The conflict can be eased through the use of a kind of automatic
programming in which fast, specialized programs for a collection of related
tasks are constructed automatically. This style of automatic programming
enterprise---which may be referred to as special-purpose automatic
programming---differs in several respects from the better known variety in
which programs are automatically derived from logical specifications.
First, the primary aim of special-purpose automatic programming is
efficiency rather than replacement of human programming effort, although
there is of course substantial overlap between these aims. Second, special-purpose
automatic programming is far more tractable at the current stage
of knowledge than the other variety, since the class of programs to be
generated by any one synthesizer of special-purpose programs is
comparatively small.  We propose to continue our current efforts in
special-purpose automatic programming, with emphasis on applications to
computer graphics and computer vision.  The problems in graphics and
vision that will be attacked take the form of automating the generation
of programs that are specialized to the task of rapidly displaying---or
recognizing---particular three-dimensional objects.

In both computer graphics and computer vision a geometric computation is
undertaken which involves three pieces of information: (1) a physical
configuration C of objects in space, (2) a position and orientation P of
the viewer relative to C, and (3) a digital image I.  In computer
graphics, I is computed from C and P; in computer vision, C and P are
computed from I.  In many practical applications of both computer vision
and computer graphics, the configuration C is fixed in advance for any
particular series of computations; it is only P and I that vary within the
batch of computations.  On the computer graphics side, an example is
provided by flight simulation, where a landscape is fixed in advance of
any particular simulated flight. The appearance of this fixed landscape
must be computed from a viewer position and orientation which changes
every thirtieth of a second.  On the computer vision side, examples are
provided by the many industrial applications of automated vision where the
vision task takes the form of recognizing and locating a particular
three-dimensional object in a digitized image.  The exact shape of the
object to be perceived is known in advance; the purpose of the act of
perception is only to determine its position and orientation in space
relative to the viewer.  Again, C is fixed in advance, while P and I vary.

Problems of the kind just described can be attacked by use of special-purpose
automatic programming.  What one does is to generate a special-purpose
program $P↓C$ for each configuration $C$ to be dealt with; this
special-purpose program is then used for each computation in which the
configuration $C$ appears.  The advantage of this approach is speed.
Since the special-purpose program $P↓C$ has a very limited task to
perform---it is adapted to handling just one configuration---it can be
much faster than any general-purpose program would be for the same
configuration.

Computer graphics and vision are good applications for special-purpose
automatic programming for several reasons.  First, there is much to be
gained since speed is of central importance in many practical
applications.  Second, the various applications within computer vision and
graphics have enough in common that fairly specific tools developed for
one application nonetheless carry over to others.  Examples will be given
later in this proposal.  Finally, automatic deduction plays a central role
in all varieties of automatic programming, including the special-purpose
variety.  Each application of automatic programming gives rise to a
different class of propositions whose truth values need to be decided
automatically.  The propositions which arise in graphics and vision
applications are for the most part simple geometric assertions.  A well
developed technology for deciding geometric propositions exists---notably
in the form of decision procedures such as the simplex algorithm for
restricted classes of geometric problems.  Applications of special-purpose
automatic programming to graphics and vision derive a substantial part of
their power from this existing technology for automatic geometric
deduction.

Goad started work on the application of
special-purpose automatic programming to computer graphics in early 1981;
work on applications to vision began in mid-1982.
As reported below, good results have been obtained for the hidden surface
elimination problem in computer graphics.  Work on vision is 
still underway, but the
preliminary results look very promising.

The same general scheme
has been employed for both applications, and there is also substantial overlap
in the specific machinery needed to implement the scheme.
In particular a central process in both applications is the automatic
design of an appropriate case analysis for the solution of the problem.
This case analysis design involves dividing up the class of possible
geometric configurations into subclasses within which regular behavior can
be obtained.  In vision the restriction to regular behavior amounts to a
requirement that the visibility of features be determined and also that
the relationships among them depend in a smooth way on the position and
orientation parameters.  In graphics regular behavior amounts to
the requirement that a single back-to-front ordering of
the surface elements to be displayed be valid within the case at
hand.  In both graphics and vision, exhaustive forms of the case analysis
are obtained from general purpose algorithms, and their final, more
efficient form is obtained by a specialization process which depends
heavily on geometric automatic deduction.  The role of automatic deduction
is essentially that of determining which sets of relevant geometric
conditions (relevant to regularity in the appropriate sense) can co-occur,
and which cannot.

Based on our experience so far, we think it very likely that a wide class
of related applications in graphics and vision can be attacked with a
comparatively small collection of tools for the automatic synthesis of
special-purpose programs.  The tools will lie at two levels of generality.
First, there are absolutely general tools for program manipulation (such as
unfolding and pruning) which are completely independent of subject matter,
and, second, there are tools which apply to a variety of algorithmic
problems within a particular mathematical domain.  The mathematical domain
which underlies the class of problems which we have chosen is
three-dimensional geometry, and the domain-specific (but not problem-specific)
tools that we use include tools for the systematic construction of
geometric case analyses and for geometric deduction.  Three-dimensional
geometry is a good choice for this kind of work since, as a result of a
vast amount of previous effort, there are many existing tools and methods
to be exploited.

\ssect Accomplishments.


\ni 1. A program for synthesis of special-purpose hidden surface 
elimination programs has
been implemented and tested on a large-scale example provided by the
Link-Singer Corporation. On this example, the generated program was 10 times
faster than the fastest and most widely used of the previously known algorithms.
This work is described in \ref:Goad.1982..

\ni 2. A synthesis method for special-purpose vision programs has been
designed and partly implemented.  The special-purpose vision programs
which are generated have the task of recognizing and locating particular
objects in an image.  The general scheme employed for object recognition
involves sequential matching of object features to image features.  By
exploiting the advance information available about the object being
sought, very large speed-ups (perhaps as much as 100-fold) can be
obtained.  The practical outcome is that the `high-level' aspects
(that is, the matching process) of model-based 3-dimensional vision can be made
fast enough for industrial applications---even when running on a
micro-processor.

\sect Epistemology and Formalization of Concurrent and Continuous Action.

Yoram Moses is currently working on the epistemology and formalization of
concurrent and continuous action. A key barrier to progress in artificial
intelligence is that present systems deal mainly with discrete events that
result in a definite new situation rather than with events occuring
concurrently and continuously. This work bears some relation to concurrent
programming, but there are some definite differences. The synchronization
problem, crucial in the concurrent programming case, seems less central
here, whereas the handling of partial information and causality are more
important for an artificial intelligence program.

Hans Berliner's thesis presents a chess position that is a forced win for
white, but this fact is not straightforwardly computable in a `reasonable'
amount of time.  Further, it appeared to McCarthy that the natural proof
of this fact involves an essentially concurrent argument.  A proof has
been worked out in detail which uses a bottom-up approach and does not use
concurrent arguments. Thus this is no longer a valid example problem.

The examples that are being considered now involve real-world activities,
such as the decision-making needed to cross a street without being hit
by a car and to pass by a revolving sprinkler without getting wet.
Both of these problems require observation and prediction of continuous
events as well as the concurrent activity of the agent and the surrounding
environment.

Eventually it is hoped that a system could be built that would be capable
of guiding a robot in a competitive two-sided sport such as tennis. Of
course that is a long term goal, and the first steps in that direction
will be pursued.

In epistemology, some special cases of McCarthy's circumscription are
being analyzed, specifically the propositional case, and generalizations
and insight into circumscription are expected to result.

A paper is being prepared dealing with the representation and encoding of
relations by graphs. This paper will be presented at the SIAM Symposium on
the Applications of Discrete Mathematics held in June 1983.

\sect Proving Facts About Lisp.

Joseph Weening is investigating the systematization of proving of facts
about Lisp programs.  In contrast to earlier work, an attempt will be made
to consider the full range of Lisp programs in a dialect such as MacLisp
or Common Lisp.  The `systematic' aspect will be to represent both
programs and proofs in a framework that can be manipulated by a computer.
The main reason for doing this is to allow verification, by the computer,
of the proofs which are presented.

Earlier work in this direction (cf. McCarthy and Cartwright, Boyer and
Moore) used a subset of Lisp, generally known as `pure Lisp,' which
consists of systems of recursive functions defined by conditional
expressions and primitive functions for numeric and list manipulation.
The aspects of Lisp that are not treated in this way include (1)
assignment statements, which change the values of variables; (2)
destructive operations, which change data structures; (3) sequential
programs; and (4) non-local control structures such as CATCH and THROW.

\sect Background.

John McCarthy is Professor of Computer Science and has worked in the area
of formal reasoning applied to computer science and artificial
intelligence since 1957.  He is working on the logic of knowledge and
belief, the circumscription mode of reasoning, formalizing properties of
programs in first order logic, and a general theory of patterns.

\vfill\eject
\sect References.
\baselineskip 12pt

\makeref:Beeson.1980.{
Beeson, M., \article{Formalizing Constructive Mathematics: Why and How?} in
Richman, F.(ed.) \book{Constructive Mathematics, Proceedings New Mexico}, 1980
Lecture Notes in Mathematics 873, Springer-Verlag (1980) pp.  146--190.}

\makeref:Brooks.1981.{
Brooks, R. A., \article{Symbolic reasoning among 3D models and 2D images}, AI
Journal, vol 16, 1981.}

\makeref:Brooks.1982a.{Brooks, R. A., Gabriel, R. P.,Steele, G. L.,
\article{An Optimizing Compiler for Lexically-Scoped Lisp},
SIGPLAN 82 Symposium on Compiler Construction, ACM,
June 23--25, 1982.}

\makeref:Brooks.1982b.{Brooks, R. A., Gabriel, R. P.,Steele, G. L.,
\article{S-1 Common Lisp Implementation},
1982 ACM Symposium on Lisp and
Functional Programming, August 15--18 1982.}

\makeref:Brooks.1983.{Brooks, R. A., Gabriel, R. P.,Steele, G. L.,
\article{Lisp-in-Lisp: High Performance},
submitted to the International Joint Conference on Artificial Intelligence,
August 1983.}

\makeref:Cartwright.1980.{
Cartwright, R., \article{A Constructive Alternative to Axiomatic Data Type
Definitions}, Proceedings LISP Conference, Stanford (1980).}

\makeref:Coppo.1980.{
Coppo, M. Dezani-Ciancaglini Venneri, B.,
\article{Principal Type Schemes and Lambda Calculus Semantics}
in Seldin, J. P. Hindley, J. R. (eds.) 
\book{To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism},
Academic Press (1980)
pp.535--560.}

\makeref:Creary.1982.{
`\article{A Language of Thought for Reasoning About Actions},  (unpublished working
paper on NFLT, June, 1982).}

\makeref:Creary.1983.{
\article{On the Epistemology of Commonsense Factual Reasoning:  Toward an Improved
Theoretical Basis for Reasoning Programs}, (forthcoming Stanford CS Report).}

\makeref:Feferman.1974.{
Feferman, S.,
\article{A Language and Axioms for Explicit Mathematics}
in Dold, A. and Eckman, B. (eds.) \book{Algebra and Logic},
Lecture Notes in Mathematics 450, Springer-Verlag (1974)
pp.87--139.}

\makeref:Feferman.1977.{
Feferman, S.
\article{Theories of Finite Type Related to Mathematical Practice}
in  Barwise, J. (ed.)
\book{Handbook of Mathematical Logic},
North-Holland 
pp.913-971.}

\makeref:Feferman.1979.{
Feferman, S.,
\article{Constructive Theories of Functions and Classes}
in Boffa, M., vanDalen, D., and McAloon, K.(eds.)
\book{Logic Colloquium 78}, University of Mons, Belgium (August 1978)
North-Holland (1979)
pp. 159--224.}

\makeref:Feferman.1981.{
Feferman, S.,
\article{Theories of Variable Finite Type},
(draft).}

\makeref:Feferman.1982.{
Feferman, S.,
\article{Inductively Presented Systems and the Formalization of Meta-Mathematics} 
in vanDalen, D., Lascar, D.,and Smiley, J. (eds.)
\book{Logic Colloquium 1980},
North Holland 1982
pp. 95--128.}


\makeref:Fenstad.1980.{
Fenstad, J. E.,
\article{General Recursion Theory: An Axiomatic Approach}
Springer-Verlag.}

\makeref:Gabriel.1982.{
Gabriel, R. P., Masinter, L. M.,
\article{Performance of Lisp Systems},
Proceedings of the 1982 ACM Symposium on Lisp and Functional
Programming, August 1982.}

\makeref:Gabriel.1983.{
Gabriel, R. P., Griss, M. L.,
\article{Lisp on Vax: A Case Study},
in preparation.}

\makeref:Goad.1982.{
Goad, C. A., \article{Automatic construction of special purpose programs for
hidden surface elimination}, Computer Graphics, vol. 16 No. 3, July 1982,
pp. 167--178.}

\makeref:G\"odel.1958.{
G\"odel, K.,
\article{On an Extension of the Finite Standpoint Never Used Before 1958},
Dialectica 12 (1958).}

\makeref:Hindley.1969.{
Hindley, R.,
\article{The Principle Type-Scheme of an Object in Combinatory Logic},
TAMS 146
pp. 29--60.}

\makeref:Ketonen.1982.{Ketonen, J., Weening, J.,
\article{EKL---An Interactive Proof Checker}, user's reference manual,
in circulation.}

\makeref:Ketonen.1982.{Ketonen, J., Weyhrauch, R.,
\article{A Decidable Fragment of Predicate Calculus}, submitted for
publication.}

\makeref:Kleene.1952.{
Kleene, S. C.,
\article{Introduction to Metamathematics},
Van Nostrand.}

\makeref:Manna.1969.{
Manna, Z.,
\article{The Correctness of Programs},
J Computer and System Sciences 3,
pp. 119--127.}

\makeref:Manna.1978.{
Manna, Z.,
\article{Six Lectures on The Logic of Computer Programming},
SIAM CBMS-NSF Regional Conference Series in Applied Mathematics No. 31 (1980).}

\makeref:Martin-Lof.1979.{
Martin-Lof, P.,
\article{Constructive Mathematics and Computer Programming},
International Congress of Logic Methodology and Philosophy of Science
(to appear).}

\makeref:McCarthy.1959.{
McCarthy, J., \article{Programs with Common Sense},
Proc. Int. Conf. on Mechanisation of Thought Processes, Teddington, England, 
National Physical Laboratory, (1959).}

\makeref:McCarthy.1963.{
McCarthy, J.,
\article{A Basis for a Mathematical Theory of Computation}
in Braffort, P. and Herschberg, D. (eds.), \book{Computer Programming and
Formal Systems},
North-Holland  (1963)
pp. 33--70.}

\makeref:McCarthy.1982.{
McCarthy, John, \article{Coloring Maps and the Kowalski Doctrine}.}

\makeref:Milner.1978.{
Milner, R.,
\article{A Theory of Type Polymorphism in Programming},
J Comp.Sys.Sci 17,
pp. 302--321.}

\makeref:Moschovakis.1969.{
Moschovakis, Y. N.,
\article{Abstract First Order Computability I, II},
Trans.Am.Math.Soc. 138 (1969),
pp. 427--464, 465--504.}

\makeref:Norstr\"om.1981.{
Norstr\"om, B.,
\article{Programming in Constructive Set Theory: Some Examples},
Proc. ACM Conference on Functonial Programming and Languages and 
Computer Architecture (October 1981),
pp. 141--153.}

\makeref:Platek.1966.{
Platek, Richard A.,
\article{Foundations of Recursion Theory},
PhD Thesis, Stanford University, 1966.}

\makeref:Scott.1975.{
Scott, D.,
\article{Data Types as Lattices},
SIAM J. Computing 5(1976)
pp. 522--587.}

\makeref:Scott.1977.{
Scott, D.,
\article{Identity and Existence in Intuitionistic Logic}
in Fourman, M. P., Mulvey, C. J., and Scott, D. (eds.),
\book{Applicatons of Sheaves, Proceedings Durham 1977},
Lecture Notes in Mathematics 753, Springer-Verlag (1979)
pp. 660--696.}

\makeref:Steele.1975.{
Steele, G. L., Sussman, G. J.,
\article{SCHEME: an Interpreter for Extended Lambda Calculus},
MIT AI Memo 349 (December 1975).}

\makeref:Tennant.1975.{
Tennant, N.,
\article{Natural Deduction for Restricted Quantification Identity and Descriptions},
5th International Congress of Logic Methodology and Philosophy of Science (1975)
pp. I--51.}

\makeref:Thatcher.1979.{ Thatcher, J. W., Wagner, E. G. and Wright, J. B.,
\article{Data Type Specification:Parameterization and the Power of
Specification Techniques}, IBM Research report RC-7757 (1979).}

\vfill\eject
\ctrline{DEDUCTIVE PROGRAMMING}

$$\vcenter{\halign{\lft{#}\cr
Zohar Manna, Professor\cr
Computer Science Department\cr
Stanford University\cr}}$$
 
\initsect
\sect Motivation.
\save2\hbox{\count0}
 
The goal of research on program synthesis is to apply the problem-solving
ability of the computer itself to the automation of the programming task.
Program Synthesis attempts to transfer the burden of programming from
person to machine. Its goals are  
to reduce the time, effort, and expertise necessary to produce
a program; to make programs more reliable; to make them easier to
maintain and modify; and to make computers accessible to people without
specialized computer training.
 
To use a program synthesis system,
a person expresses the purpose of the desired program in a
``speci\-fi\-ca\-tion.''
This speci\-fi\-ca\-tion states {\sl what} the program is intended to
achieve, but not {\sl how} it is to achieve it.  The method or ``algorithm''
to be employed by the program need not be spelled out in the
speci\-fi\-ca\-tion; the design of the algorithm is the responsibility
of the system. The system guarantees that the final program satisfies the
given specification; there is no need for subsequent verification
or debugging.

The ideal speci\-fi\-ca\-tion language is as close as possible
to the terms in which a person thinks about the problem to be solved.
This makes it unnecessary for us to paraphrase our thoughts in formulating
a speci\-fi\-ca\-tion. For most people, natural language, diagrams, and
examples, say, are direct means of expression.  If the program deals with
a specific subject area, traditional notations peculiar to that subject
area may be appropriate. 

Many program synthesis researchers, however,
tend to use logic-based speci\-fi\-ca\-tion languages, which are
unambiguous, uniform, and easy for computers to understand and
manipulate.  Ultimately, languages people find more convenient for
speci\-fi\-ca\-tion can be translated internally into a logic-based language.
 
Writing a specification is easier than writing a program
for several reasons: First, because we do not have to design an
algorithm, but only to state the conditions the algorithm is intended to
satisfy. Also, because the speci\-fi\-ca\-tion language can be designed
exclusively for ease of expression, completely disregarding
implementation concerns that constrain a programming-language designer.
 
Of course, we may make errors in formulating a speci\-fi\-ca\-tion;
we may misstate a condition the program is intended to satisfy. 
In constructing a complex computer program, a person will
generally not know exactly what he wants; therefore, the speci\-fi\-ca\-tion he
formulates will not reflect his intentions accurately, no matter how expressive 
the
speci\-fi\-ca\-tion language he uses.  Typically, he will neglect to include
conditions the program is meant to satisfy. The conditions he has
included, each expressing a different demand, will contradict one
another. A carefully phrased condition may describe behavior that he
does not really want at all.  In normal programming practice, these
discrepancies will not be noticed until the implementation is
under way or, indeed, until the program is ``complete'' and is put
into use.
 
Nevertheless,
because the speci\-fi\-ca\-tion expresses what the person wants directly, in language
close to the terms in which he thinks about the problem, and because 
speci\-fi\-ca\-tions are typically much shorter than the programs that achieve
them, bugs in speci\-fi\-ca\-tions are less frequent than those in programs.
Although there is no way a synthesis system can detect
whether a person has formulated his intentions accurately, the discipline
of writing a speci\-fi\-ca\-tion will make some omission, inconsistency,
and misdirection obvious. Furthermore, the same techniques we apply to
synthesize programs may also be employed for ``running''
speci\-fi\-ca\-tions automatically, to examine the behavior
they describe for unpleasant surprises.  In this way, we can test a
speci\-fi\-ca\-tion before the program is actually developed.
 
The final program could be produced in any programming
language.  Techniques for constructing applicative (side-effect-free) 
programs are currently the most highly developed; 
we tend to use a simple LISP-like
applicative language with conditional (if-then-else) expressions
and recursive function calls.  But there is no difficulty in
translating from such a language into any of the other computer
languages commonly in use, or to develop the program in any of these
languages directly.
 
\sect The Approach.

To construct a program from a specification requires a knowledge 
both of programming technique and 
of the subject area of the program to be constructed, as well as the reasoning
ability necessary to apply this knowledge effectively when faced
with a new problem. Techniques obtained from problem solving, theorem
proving, and expert systems have all been brought to bear on
the synthesis problem.

We are pursuing a {\sl deductive approach}, which
relies on automated theorem-proving techniques to manipulate knowledge
represented as axioms and inference rules. The problem of constructing a program
is rephrased as one of proving a theorem. For example, to construct a
program producing an output that satisfies certain properties, we prove a
theorem establishing the existence of an object with these properties.
The proof is restricted to be constructive, in the sense that a program
producing the desired output, expressed in terms of the programming
language, may be extracted from the proof.  Thus, in proving the
existence of the object, we also discover how to compute it. 
The structure of the final program reflects the form of the proof by which
it was produced. Thus, case analysis in the proof yields a conditional
expression in the program; mathematical induction in the proof yields recursion 
in the program. Different proofs of the same theorem lead to different
programs, all satisfying the same specification.

Knowledge of the subject matter of the desired program, of the language
in which the program is to be expressed, and of the skills and techniques
of the programmer are represented as the axioms and rules
of the deductive system that proves the theorem.  
This method of construction provides an implicit proof that the program
satisfies its speci\-fi\-ca\-tion. Another
advantage of this approach is that, over
the years, many theorem-proving techniques have been developed,
which can be applied directly to the program synthesis problem.
 
We have devised a {\sl deductive tableau} theorem-proving formalism [7]
particularly well-suited for the program synthesis application.
This formalism, described in detail in our forthcoming book [11],
combines elements of nonclausal resolution transformation (rewriting)
rules, and mathematical induction within a unified framework.

Although contemporary theorem-proving systems cannot solve
the problems of interest to research mathematicians, we do not require
this level of ability for most program synthesis.  Rather, we need to prove
routine theorems at a level of detail a person would find
tedious. As theorem-proving techniques improve, 
as better hardware is made available,
and as systems with large numbers of parallel processors become 
common, we can expect methods that are now of only academic interest to
become everyday tools.
 
Although fully automatic program synthesis may not become feasible for
some time, the same techniques may be applied interactively much sooner.  
Interactive
systems for program synthesis, program transformation, and program
maintenance can all be developed with existing hardware and
program synthesis technology.
 
Under an interactive system, there arise choices between 
alternative avenues in the program development process.
Some of these approaches
will ultimately lead to a solution, while others lead to a stalemate or, even
worse, continue interminably without a decisive
success or failure. Thus, constructing a program may be compared to
finding our way through a maze, some of whose paths are infinite. 
Although heuristic methods may guide
an automatic system in making some of the choices, people are more adept at it.
An interactive system allows a human collaborator to use his intuition
to influence the choice; the more
routine steps are still performed by the system. Thus, the system carries
out the intricate details of a program's derivation, and guarantees the
correctness of the final proram, but is guided in 
its major decisions by the human collaborator.
 
Like the program's speci\-fi\-ca\-tion, the decisions to be made
can be expressed in terms that are easy for a person to understand. 
The collaborator
must be familiar with the terminology of the subject area of the program to be
constructed, but he does not need to know the programming language or the
specialized jargon of the computer professional.
The advice given by the human collaborator need not be perfect. A bad choice
will delay the construction of a program; repeated bad choices can postpone
it indefinitely. But bad advice can never cause the system to construct a
program that fails to meet its specification.

\sect Recent work.
 
Manna and Waldinger have worked on program synthesis since 1968 (e.g.,
see [5]). They collaborated on the implementation of the DEDALUS  
program synthesis system [6], which applied a transformational
approach, under which the program was constructed by applying
transformation rules directly to the program's specification.
Since 1978, Manna and Waldinger have been pursuing the new
deductive approach. An automatic version of part of that system has
been implemented by Stickel [13]; an interactive version has been
implemented by Malachi [4].

The deductive approach was initially oriented toward the synthesis of
applicative programs, programs which yield an output but do not assign
values to variables, alter data structures, or produce other side effects.
A {\sl situational-calculus} formalism has been devised to extend the
deductive approach to the synthesis of nonapplicative programs [8].
According to this approach, the specification for the program, and the 
description of the available programming-language constructs, are 
expressed in terms of a situational calculus, which refers explicitly
to the states of the computation.
 
Work is underway [9] to give the deductive-tableau formalism special
abilities to deal with commonly used relations, including equality and
ordering relations. These abilities result in shorter derivations and a
dramatically reduced search space in the synthesis of programs that rely
on these special relations.
 
The deductive approach has been applied to the synthesis of several
nontrivial programs. For example, a detailed synthesis of a version of
Robinson's unification algorithm was devised [10]. 
Portions of that derivation have since been reproduced by interactive
systems of Eriksson [3] and Paulson [12].

\sect Related work.

The program synthesis research of Green and of Balzer (see, e.g. [1]) 
is based on
a ``transformational'' approach, in which equivalence-preserving transformation
rules are applied directly to the specification of the desired program, until 
eventually the program is produced.  Although we worked on this approach earlier
(e.g., the DEDALUS system), we abandoned it in favor of
our current deductive approach. 

There are major technical differences between the two approaches.  Some
of the advantages of the deductive approach over the transformational approach
are as follows:

\BBpar{The  transformational  approach  requires a  separate  deductive
component (i.e., a  theorem prover),  e.g., to  establish
the side-conditions  for  applying transformation  rules  or  to
prove the termination of the program under construction.   Under
the deductive approach,  the deductive component  is the  entire system.}

\BBpar{The deductive approach  enables us to  take advantage of  recent
improvements in theorem-proving  technology, such as  nonclausal
resolution, relational polarity, improved unification algorithms,
and  fast  decision  procedures.   Each  new  technique  may  be
incorporated directly into the synthesis system.}

\BBpar{Under the deductive  approach, the construction of  conditionals
(tests) and  recursive calls  (loops) in the  program is  the
natural by-product of the use of case analysis and  mathematical
induction,   respectively,    in   the    proof.    Under    the
transformational approach,  the  formation of  conditionals  and
recursive calls require special mechanisms.}

Program synthesis is a search problem, and both transformational and
deductive systems face the same difficulty in deciding what rule to apply at
each point.  The same information may be used to choose a transformation rule
under the transformational approach or to choose a deduction rule under the
deductive approach.

Neither the deductive approach nor the transformational approach is
inherently ``knowledge-based.''  Large amounts of specific subject-domain and
programming knowledge may be represented under either approach.  The work of
Green and of Balzer, however, concentrates on the ``knowledge'' aspects of the 
problem, while our work emphasizes its ``logical'' aspects.  Both directions are 
essential to the development of practical program synthesis systems.

\sect Research Directions.
 
We anticipate that program synthesis techniques are about to alter
radically the way computer programs are produced. There are several
research directions could advance program synthesis research in several
directions.

\bite {\sl Interactive Program Synthesis}
 
Our experimental system ([4]) requires the user to direct the
system by indicating explicitly the next major rule to be applied at each stage.
Ideally, the user should not require such an intimate knowledge 
of the system's inner workings. Rather, the system should explain the
legal alternatives to the user in the familiar terminology of the
specification language, and the user should merely choose among them.
 
\bite {\sl Program Maintenance}
 
Programs produced by a synthesis system are particularly easy to maintain
or alter. After the synthesis is complete, the
{\sl derivation structure}, i.e., the entire
record of the development, may be retained. This structure will indicate what
condition each portion of the program is intended to achieve, and how
that condition is related to the program's speci\-fi\-ca\-tion.  Systematic
techniques are being investigated so that when the
speci\-fi\-ca\-tion changes, the system can then alter only those portions
of the program required to respond to the change. The system will also
ensure that the altered program will continue to meet those conditions
of the speci\-fi\-ca\-tion that have not been changed.
 
\bite {\sl Program Transformation}
 
Program transformation is a process of systematically
rewriting a program without altering its external behavior, generally 
for the purpose of improving its efficiency. 
Program transformation may be regarded as a 
special case of program synthesis in which the original program serves
as the speci\-fi\-ca\-tion for its improved version. The same techniques a
synthesis system uses to construct a program may be used to improve
one.
 
If a synthesis system is given access to the speci\-fi\-ca\-tion 
for the original program as well as to the program itself, it should be able
to effect more radical transformations --- for example, altering the program
to produce a different output, if that output satisfies the same
speci\-fi\-ca\-tion and can be computed more efficiently. Ideally, the system
should be given the entire derivation structure of the program before
beginning to transform it.
 
\bite {\sl Monitoring Efficiency}
 
If the system is automatic, it must monitor the program's 
efficiency as it is being constructed. Approaches leading to
inefficient programs can then be cut off as the inefficiency is detected.
Efficiency requirements may possibly be included in the speci\-fi\-ca\-tion;
in constructing the program, the system would then be required to prove
that these requirements have been met and, if they have not, 
to continue the development.
In this way, the final program would be guaranteed to meet
the given efficiency requirements. Such requirements, however, are not always
easy to prove.
 
The preceding technique could also be employed in an
interactive system.  Alternatively, the efficiency could be monitored
by the human collaborator. Typically, an initial program would be
produced with complete disregard for efficiency concerns. The performance
of that program could then be improved in a subsequent transformation
phase.

\bite {\sl Mathematical Induction and Generalization}
 
The mathematical induction rule is essential to deductive program synthesis
because it is the basis for the formation of recursive programs and all
other repetitive constructs. Special demands are made on a theorem prover by the
induction rule because before an inductive proof will succeed,
the theorem to be proved may need to be generalized.
Although a novel generalization
facility is described in our original deductive-approach paper, the details
have not yet been spelled out and the facility has not yet been implemented.
 
\bite {\sl Deductive Programming Language}
 
The system of axioms and deductive rules we have developed to construct
programs can itself be regarded as a programming language. Such a language 
combines some of the advantages of PROLOG and LISP, but is higher-level and
more expressive than either. In particular, as in PROLOG, programs may be 
read as declarative sentences rather than imperative commands; as is LISP,
programs may invoke both functions and predicates. A rich variety of data
structures is provided, including lists, trees, sets, and expressions.
The success of this enterprise would depend on the development of a 
high-speed special-purpose deductive-tableau theorem prover, bearing the same
relationship to the general theorem prover as a PROLOG implementation
bears to a general resolution theorem prover (see e.g. [2]).
 
\bite {\sl Synthesis of Concurrent Programs}
 
Although applicative programs may easily be evaluated concurrently, special
problems involved with the interaction of side-effects occur in the synthesis
of concurrent nonapplicative programs. For human programmers, the development
of correct concurrent programs is still something of a black art. We plan to
extend our situational-calculus formalism for sequential programs to allow the
synthesis of concurrent programs within the deductive-tableau framework.
 
\bite {\sl Automatic Synthesis}
 
Although interactive systems offer the most immediate practical results, they
will ultimately be overtaken by more automatic systems. We plan to gradually
integrate heuristic considerations into the deductive tableau formalism.
Metalevel sentences seem to offer the most likely way of representing strategic
knowledge.
 
\bite {\sl Planning}
 
Because programs may be identified with plans, any program synthesis system
may be regarded as a planning system. New program synthesis techniques often
have unforseen benefits when transferred to the planning domain. We intend
to examine the application of our results to planning problems.
 
\sect References.
\baselineskip 12pt

\numitem{1.}A. Barr and E. A. Feigenbaum (eds.), ``The Handbook of Artificial
Intelligence,'' Volume II, HeurisTech Press, Stanford, CA (1982).

\numitem{2.}W.F. Clockson and C.S. Mellish, ``Programming in Prolog,'' Springer-Verlag (1981).

\numitem{3.}L.H. Eriksson, ``Synthesis of a Unification Algorithm in a Logic
Programming Calculus,'' Technical Report, Department of
computer Science, Uppsala University, Uppsala, Sweden (Jan. 1983).

\numitem{4.}Y. Malachi, ``Deductive Programming Approach and Implementation,''
Computer Science Report, Stanford University, Stanford, CA (1983, to appear).

\numitem{5.}Z. Manna and R. Waldinger, ``Toward Automatic Program Synthesis,''
{\sl Communications of the ACM}, Vol.\ 14, No.\ 3 (March 1971), 151--165.

\numitem{6.}Z. Manna and R. Waldinger, ``Synthesis:  Dreams => Programs,'' {\sl IEEE
Transactions on Software Engineering}, Vol.\ SE-5, No.\ 4 
(July 1979), 294--328.

\numitem{7.}Z. Manna and R. Waldinger, ``A Deductive Approach to Program Synthesis,''
{\sl ACM Transactions on Programming Languages and Systems}, Vol.\ 2,
No.\ 1 (January 1980), 90--121.

\numitem{8.}Z. Manna and R. Waldinger, ``Problematic Features of Programming
Languages: A Situational-Calculus Approach,'' {\sl Acta Informatica},
Vol.\ 16 (1981), 371--426.

\numitem{9.}Z. Manna and R. Waldinger, ``Special Relations in Program-Synthetic
Deduction,'' {\sl Journal of the ACM} (to appear in 1983).

\numitem{10.}Z. Manna and R. Waldinger, ``Deductive Synthesis of the Unification
Algorithm,'' {\sl Science of Computer Programming}, Vol.\ 1 
(1981), 5--48.

\numitem{11.}Z. Manna and R. Waldinger, ``Logical Basis for Computer Proramming,''
textbook, two volumes (1983, to appear).

\numitem{12.}L. Paulson, ``Recent Developments in LCF: Examples of Structural
Induction,'' Technical Report No. 34, Computer Laboratory, University
of Cambridge, Cambridge, England (Jan. 1983).
 
\numitem{13.}M.E. Stickel, ``A Nonclausal Connection-graph Resolution Theorem-proving
Program,'' in Proceeding of the National Conference on Artificial 
Intelligence, Pittsgurgh, PA (Aug. 1982).

\vfill\eject
\ctrline{RESEARCH IN THE ANALYSIS OF ALGORITHMS}

$$\vcenter{\halign{\lft{#}\cr
Donald E. Knuth, Professor\cr
Computer Science Department\cr
Stanford University\cr}}$$

\initsect
\sect Introduction.
\save3\hbox{\count0}

Professor Knuth and his associates are interested in three areas of
research:  (1) To create efficient new computer methods for important
practical problems. (2) To create better mathematics in order to determine
how efficient such methods are. (3) To extend programming methodology so
that such algorithms can be implemented more quickly and reliably than
with current techniques. These three areas of research mutually support
each other; advances in each one lead to advances in the other two.

\sect Research Directions.

More specifically, under (1) we are currently working on (a) new
algorithms for digital raster graphics, on (b) new algorithms
for the combinatorial matching problem, and on (c) new algorithms
for the ``all nearest neighbor'' problem.

(1a) Curved lines can be satisfactorily approximated by cubic spline
functions, where the coordinates of the points $(x,y)$ on the curve
are given by the formulas
$$\eqalign{     x ⊗= x↓0 + x↓1 t + x↓2 t↑2 + x↓3 t↑3 \cr
                y ⊗= y↓0 + y↓1 t + y↓2 t↑2 + y↓3 t↑3 \cr}$$
as $t$ varies from 0 to 1. However, existing methods of plotting
such curves require a substantial amount of computer time. We believe
that it is possible to plot any cubic spline with a very efficient
new method that involves only addition, subtraction, and testing the
sign of a register, with all computations on integers. If our
preliminary guesses prove to be true, the new method will be ideal
for implementation in hardware, because it computes the curve
in ``real time'' in much the same way as well-known methods for
plotting circles, and because it requires only three times as
much computational machinery as is necessary for circles.

(1b) The combinatorial matching problem consists of determining
whether it is possible to arrange $2n$ elements into $n$ pairs,
subject to the restriction that all pairs must be chosen from
a given set of ``feasible'' pairs. This fundamental problem
has been shown to have numerous applications, and to be a stepping
stone to the solution of other problems for which a brute-force
search of the possibilities would take thousands of years to
complete. It is problems like these where good ideas save many
orders of magnitude of computer time. We believe that it is possible
to find a faster matching algorithm than those already known,
by developing sophisticated new data structures for representing
the manipulations inside the computer.

(1c) The ``all nearest neighbors'' problem consists of taking
a set of $n$ points in $d$-dimensional space and, for each point,
determining which other point is closest to it. We believe that
it will be possible to solve this problem with a new method
whose running time is a constant times $n \log n$; the constant
depends on the dimension $d$. The best methods currently known
for this problem require running time proportional to
$n (\log n)↑{d-1}$. Furthermore this new method should lead to improved
algorithms for other geometric optimization problems, such as
the minimum spanning tree that connects a given set of points.

Under area (2) we are currently looking at problems of random
mappings, which are fundamental to numerous applications, including
cryptanalysis. A mapping on a set can be thought of as a collection
of individuals each of whom is pointing a finger at another
individual. In the applications it is important to study questions
of the following type: Start with an individual $x↓0$ chosen
at random; let $x↓0$ point to $x↓1$, who points to $x↓2$, and so
on. Eventually there will be a cycle, i.e., $x↓{m-1}$ will point
to $x↓m$, where $x↓m$ has already been named ($x↓m=x↓k$ for some
$k$ less than $m$). The problem is to figure out how large $m$ is
likely to be. For example, if $m$ is not too large, it is possible
to ``crack'' certain codes; furthermore, this problem relates to
the efficiency of a variety of other algorithms. We are looking
at special cases of the problem that have never been solved;
in particular, we want to know the answer when half of the individuals
are pointed to by two others, while the other half are never pointed to
at all. We believe that we are on the verge of a breakthrough in
understanding this sort of problem, and that this understanding will
have a payoff in the design of new computer methods.

Finally, under area (3) we believe that our current research is likely to
have a significant effect on the way all large-scale computer software
will be written in the future. Professor Knuth has made successful
preliminary studies with a new system called WEB, which promises to
improve greatly the present state of the art in the documentation of
computer programs. We believe that this not only makes programs easier to
read and to maintain, but that it makes them more reliable and of higher
quality in the first place; yet it takes no longer, and the new system is
actually more pleasant to use than existing methods. These are obviously
strong claims, but the preliminary experiences have indeed been enormously
encouraging.  Therefore we plan to greatly increase the usage of WEB in
our own software tools, and to use it exclusively in the new algorithms
that we develop, so that this project will serve as a testbed for
the new methodology. In this way we believe that the example WEB programs
we write will provide a model for a new style of programming that may
well improve the quality of all major computer programs.

The WEB system is a combination of a traditional computer programming
language with a document-formatting language. When the two are blended
together in the right way, we obtain a system that is much more powerful
than when either system is used by itself, and it leads to the advantages
claimed above. The concept is new and cannot be explained easily in a few
paragraphs.  During the next year or two we should be able to prepare
reports that will convince a substantial number of people outside Stanford
to use this method.

\vfill\eject
%Data Base Research
\par\dispskip\par
\ctrline{MANAGEMENT AND USE OF KNOWLEDGE}

$$\vcenter{\halign{\lft{#}\cr
Gio Wiederhold, Assistant Professor\cr
Computer Science Department\cr
Stanford University\cr}}$$
 
\initsect
\sect Summary.
\save4\hbox{\count0}

Distributed and centralized data systems are central to the management
functions of modern enterprises.
Systems to store data include heterogeneous computer networks 
as well as centralized collections of data on files maintained by a variety
of programs.
To make effective use of such data the {\sl knowledge} we have about the 
data has to be formalized in such a way that it can be automatically exploited.

\sect Rationale.

In the electronic society control of information is paramount. Managers
are aware of the value of control (and access) to information. They are
naturally resistant to loss of control  of the data developed and used 
by their enterprises.  
Loss of control is perceived to be concomitant 
with the centralization implied by large databases.

While economic and technological considerations have
favored the centralization of data storage and processing during the
past few decades, recent directions in hardware development and VLSI
design suggest that the future will bring networks of smaller, yet
powerful, special purpose computers, that can be used to collect, store,
and process information closer to its source.  Loosely-coupled networks
of different machines, personal workstations, etc. are likely to be the
dominant type of computing environment within a few years. Consequently,
local control of local information will be the rule rather than the
exception.  Such distributed environments pose new difficulties for the
management of data resources.

The utility of computers and computer-based systems in large
organizations has been limited more by inadequate techniques for
managing large quantities of data than by our technical ability to
gather and store that data. Existing systems for collecting,
representing, and retrieving information are too inflexible and complex
for easy extraction of information. The generation of large reports and
the execution of well-formed transactions for queries produces data,
rather than information.  Typically, several layers of management and
technical staff intervene between data and its users, hampering
effective and efficient decision making based on information stored
within databases.

Developments in Artificial Intelligence over the last few decades
provide tools that can be of value in increasing the responsiveness of
database systems to the needs of their users. To pursue our work in
applying Artificial Intelligence techniques to the practical domain of
database management, we propose to expand our area of study to include
the problems of data management in distributed computing environments.

Our research probes the boundaries of data management.
We typically determine the limits of algorithmic approaches and new technology,
 and develop heuristic methods based on Artificial 
Intelligence techniques to go beyond those boundaries.
The large quantities of data, the complexity of the relationships
being represented, and the limits of storage technology all require that
advanced techniques must be pursued if realistic problems are to be 
addressed.

New challenges for the processing of data by distributed systems, 
where the knowledge and  authority required to
intelligently manage diverse sources of information is itself
distributed among multiple sites.  Familiar methods of data management---where
perfect information about the structure, semantics, and content of
the data is normally a given---are not adequate to deal with the less
structured environment encountered in truly distributed systems.
Difficulties occur in every aspect of data management: query processing,
security, database design, redundancy, semantic modelling, optimization,
integrity, data abstraction, and decentralized processing.  What is
needed is a new set of data management tools for the new distributed
environments. Such tools should build on existing database technology,
and bring to bear the techniques developed in the Artificial
Intelligence community for dealing with partially understood,
arbitrarily structured problem domains.

Our previous work on the Knowledge Base Management Systems and the 
Management of Distributed Data (ARPA contract N00039-80-G-0132) at 
Stanford and SRI International has
demonstrated that substantial improvements in the utility of database
systems result from the application of techniques borrowed from
Artificial Intelligence. The incorporation of higher level semantic
knowledge into database systems has been shown to help with the
design, improve the manageability, and increase the utility of data in a variety
of ways.  Upgrading databases from information storing to information
understanding systems---by incorporating knowledge of the data and the
domain into the system itself---is a natural and needed dimension for
growth in such systems.

We are extending our studies to the formal and intuitive concepts
required to intelligently manage data in distributed environments, and
to develop techniques for dealing effectively with the problems
encountered.  In particular we have explored the problems that occur
when the distributed user has only a limited view from which to
manage the database.

\sect Previous Work.

From its inception in 1979, the Knowledge Base Management Systems project
at Stanford University has been concerned with exploring applications of
new algorithmic and Artificial Intelligence techniques to database systems. 
Specific areas addressed include the initial design, the operational
performance, and th use of such systems by non-computer-science professionals.
Various specific techniques  and tools to improve the utility of 
existing and future database  management systems have been developed. 
The work done to date indicates that:

\ni * Traditional, algorithmic techniques provide a solid foundation
for work in databases, but the models used cannot cope adequately with 
the complexities  and the scale of systems of realistic proportions.


\ni * The techniques developed in Artificial Intelligence research apply
well to the database world, due to the intrinsic formal abstraction
provided by databases in their modelling of the real world. Artificial
Intelligence research has been most effective where it focused on highly 
structured domains, that are subject to simplified abstract descriptions. 
Databases provide a realistic example of such a domain.

\ni * Within the KBMS framework we have been able to develop innovative
approaches to the use of task models in query processing, semantic query
optimization, modelling the database needs of diverse user groups,
integrating diverse user database models, common subexpression analysis
in query processing, natural language database update, descriptive
responses to database queries, lexicon management, the design of
portable file access systems, database technology to support VLSI
design, database machines, distributed databases, and optimal design of
centralized and distributed physical databases.

\ni * Our work is finding applications in the design and operation of
information systems in the outside world and is beginning to
contribute to tasks being undertaken by NASA, Military Manpower Planning,
and other institutions, including applications for manufacturing,  
medical, and  financial systems.

Our work concentrates on promising tasks areas within our
research definition.
Each of these areas are briefly described below.

\ssect A methodology for the design of user models.

     This area concerns research to improve the techniques of database
design and modelling.  The Structural Model, formally defined within the
KBMS project, captures those semantics that are of importance in the
design of the physical structure of the database.  In addition to
relations and tuples, inter-relation ownership, reference, and subset
connections are modelled.  In this sense the structural model can be
considered as a formalization of an important aspect of the semantic
models, for instance the Entity-Relationship models, that are used to
capture the requirements of the users.

\ssect The integration of user models into a comprehensive database model.

In order to generate a comprehensive database model many data models of
individual applications may have to be integrated, since the problem of
designing a large database involves many potential users, each having
his own perception of what the database should look like.  Our model
supports the integration of many such views into a database model to
support all users \ref:ElMasri.1977..
Included in the model is a formalism for the clear
expression of structural integrity constraints in each user's view of
the application area and rules for resolving these constraints relative
to all users. This database model can remain invariant while performance
and operational constraints cause the inplemented version of the
database to change.

\ssect Integration of diverse user models at diverse sites.

In centralized environments a database administrator is responsible for
the design of a central database that supports the diverse views of
individual users, each of whom can be aware of only a portion of the
actual database. In distributed environments there may be no single
individual with sufficiently global knowledge (or authority) to perform
this task \ref:Wiederhold.1983..  While no central database will exist, a 
comprehensive data model is critical for maintaining overall 
consistency and for performing distributed processing of queries and 
updates.  

\ssect The design of physical databases from the integrated model.

The structural model permits the attachment of projected usage factors
from the individual users, and the combined knowledge can be employed
to design an effective database implementation.  Such a database may
be based on relational, hierarchical, or network implementation concepts.

     A straightforward algorithmic optimization approach is not 
feasible since the combinations of the decision space greatly exceed 
bounds of feasible
exhaustive search.  We have however developed a method which will
provide the implementation guidelines for a relational database in close
to linear time \ref:Whang.1981..  The concept
developed is termed ``separability'' of joins between the participating
relations.  The assumptions required for this approach appear to be
fulfilled over a wide range of practical cases.  We have extended 
this approach to network databases \ref:Whang.1982..  

We have also explored the design issues in distributed systems and 
explored useful algorithms for optimality.  In this process
we have again found limits of design problem complexity which
will require the development and evaluation of heuristic approaches.

\ssect Update of data.

If the form, content, and availability of data throughout the network is
not completely known to a user or at any single site, updates that involve the
coordination of information stored beyond the immediate view
of the user must be treated with extreme care.
The structural model, which we have used and formalized
in our research, permits the description of constraints which
a view has to obey in a centralized as well as in a
heterogeneous, distributed environment.
Notions of formal correctness as well as of measures of most reasonable
updates in semantic terms have been developed \ref:Keller.1982..

A further avenue is the
investigation into the desirability of having prejoined relations,
implying replicated data.  In distributed systems this technique becomes
essential due to the greater ratio of data retrieval versus processing
costs.

\ssect Natural language database update.

     Although considerable research has studied the problem of
processing queries expressed in natural language, the possibilities for
performing natural language database updates have not been explored.
The primary difficulty is that the casual user of a natural language
system does not understand the details of the underlying database, and
so may make requests that either (a) are reasonable given their view of
the domain but are not possible in the underlying database; (b) are
ambiguous with respect to the underlying database; (c) have
unanticipated side effects on the responses to earlier questions or on
alternative views of the database.  A theory detecting the particular
user's view of the database and determining the legality, ambiguity, and
potential side effects of updates expressed in natural language has been
developed.  A formal analysis of the problems associated with updates
expressed on views (data sub-models) is central to this work.  A system
has been implemented, based on this approach, which processes natural
language updates, explaining problems or options to the user in terms
that the user can understand, and affects the changes to the underlying
database with the minimal disruption of other views \ref:Davidson.1981..

\ssect Distributed resiliency mechanisms.

An implied, but rarely realized, benefit of having a distributed database
is increased data availability in case of failures. 
Such a system is considered resilient with respect to failures, rather
than failure-proof.
A local node may not be able to provide complete local recoverability.  
This can be due to economic considerations, since the cost of local 
secure redundant storage can be excessive for small systems, or can be 
due to operation in a high risk environment.  Techniques to use other 
network nodes to effect the recoverability of failed nodes, even when 
local storage has been damaged, have been explored and documented.
We are obtaining feedback about their use in financial and manufacturing
systems \ref:Minoura.1982.. 

\ssect Structural Model application in distributed database design.

Our work on database design is based on the use of structurally 
relevant semantics, which are the basis for defined connections in the
database.  These connections in turn, when the expected usage loads are
mapped to them, provide the guidance for the physical binding design
decision which are necessary to give large databases acceptable 
performance \ref:Ceri.1982..

This issue maps directly into distributed systems: the cost
of connections that go via communication links becomes even more critical.
In distributed databases a major technique to achieve acceptable performance
is the replication of data.   We are beginning to model
this technique using the concept of an identity connection \ref:Wiederhold.1983..
When this technique is used at times in  the centralized environment
the binding can be quite rigid.
We find that the cost of maintaining rigid identity connections is quite
high in distributed systems.

\ssect Cooperative interactive interfaces to distributed databases.

In an environment where a user may have incomplete or incorrect
knowledge of the structure of available data, he may pose queries or
updates that are either unanswerable, impossible to perform, or are
otherwise misguided. Our work \ref:Kaplan.1980. has shown that such
misconceptions can often be detected directly from the phrasing of the
user's request and a knowledge of the structure of the database. This
information can be used to correct the user's misconceptions and inform
him about the nature of the database and database system. These
techniques for providing cooperative processing of transactions need to
be extended to distributed environments, where the knowledge necessary
to intelligently aid inexpert users may partially reside at remote
sites.

\ssect Experiments with database technology to support VLSI design.

     The complexity of large VLSI or device designs impacts the design
cycle.  Single designer approaches take long or utilize chip or card area
poorly, and multi-designer teams require much communication and task
scheduling.  Current design automation aids use task specific files
without automatic feedback of analysis results or decisions made by the
designers.  

We have applied our techniques to manage databases to aid the VLSI 
design process.  The database is used here as a communication
medium among people working at different levels on the same object,
namely the same device or system.  
Logic and circuit design information of two devices, a ALU and
a PDP-11 CPU, and the component library required to build them, have
been placed into a CODASYL (DBMS-20) database.  The lower level data
elements can be automatically generated using an existing design
automation program.   Performance measurements indicated only a
factor 2 performance degradation versus use of specialized design files.
Modification of lower level elements during the design process is
signalled automatically, using a height-first algorithm, to the related
parent levels, so that this detailed knowledge can be incorporated in
the higher level abstraction, when these are accessed during successive
design iterations.

We have developed some access techniques to the design data which permit
retrieval of data that is partially stored. If required elements are not
stored, they are generated from higher level circuit or logic
specifications.  Partial storage is important.  The volume of lower
level elements in a VLSI design can be greater than is manageable by the
largest storage devices now available, so that automatic methods for
VLSI design automation will need access to a mix of generatable, regular
elements and instantiated, irregular elements if they are to handle
large circuits that are not totally regular \ref:Wiederhold.1981..

We are in the process of evaluating our approaches for other database
environments to make our results more accessible to practitioners.
An important byproduct of this work will be an assessment of the
tradeoffs among database implementations models.
Much argument has been created in the arena of relational versus 
network implementations.
We believe that a solid experiment in this one critical area can 
help in quantizing the issue in an objective fashion.

We have begun to consider the issue is the automatic management of 
design versions.  This task
is performed now by databases that support engineering change control.
The same problem is being addressed in conventional databases that
are concerned with time or planning updates, but there are yet few   
results to draw upon, so that in fact the design area may be able to
lead in this research field.
 [refs from olumi]

\ssect Task models.

     Certain entities in a database---be they fields, attributes,
relations, or more complicated constructs---have certain a priori
probabilities of being required in an interrogation of the database.
These probabilities are dependent on the particular task a user may be
performing, and his or her focus and interests.  By incorporating a task
model into the KBMS, these characteristics can be used in a variety of
ways to improve the utility of the system.  Four main uses of task
models have been explored in a KBMS: (a) inclusion of relevant
information not explicitly requested in the response to a query; (b)
organizing responses so that the more ``interesting'' items are presented
first; (c) checking for semantic irregularities in the performance of
the task; and (d) prefetching of items and fields that have not yet been
requested but are likely to be in the near future.

\ssect Semantic query optimization.

A request for information can often be formulated in more than one
way, depending on knowledge about the subject area and ingenuity in
determining the best access path to the desired information.  A question
about all ships currently carrying iron ore, for example, can be
answered by only looking at information about bulk ore carriers,
assuming that it is known that only bulk ore carriers carry iron ore.


Semantic query optimization is an approach to query optimization
that uses such domain knowledge, often referred to as semantic integrity
constraints.  The objective is to transform a query into a semantically
equivalent one, one that produces the same answer, but that can be
processed more efficiently.

This work demonstrates that semantic knowledge about the database can be
used in a new way to achieve efficient data retrieval.  The method
supplements conventional query optimization methods.  It draws on
semantic, structural, and processing knowledge, and makes use of the
heuristics of query processing developed in prior research.  A system
has been implemented to explore this approach.  Improvements have been
demonstrated in a range of query types, by means of transformations that
add  or delete  constraints  on  attributes  or even  entire  files,  as
warranted by  the database  and query  structure.  In  other cases,  the
system detects  unsatisfiable query  conditions without  inspecting  the
database, or aborts inference when it determines that no improvement can
be expected.  Analysis overhead is low in all cases.
\ref:King.1979. \ref:King.1980a. \ref:King.1980b.

\ssect Descriptive responses to database queries.

     The typical response to a database query is to list the set of
items from the database that satisfy the conditions presented in the
query.  This list can be excessively long, and consequently may be
inappropriate for a conversational system.  Often, a more appropriate
response to such queries is a description of the set, rather than a
listing of its elements.  For example, the response ``All corporate
officers'' may be more concise and informative in response to ``Which
employees profit share''  than a list of 1,000 names.  Practical
techniques for producing a significant class of such responses from
existing database systems without a using a separate world model or
knowledge base have been been implemented.

\ssect Lexicon management.

     For natural language systems to provide practical access for
database users, they must be capable of handling realistic databases.
Such databases are often quite large, and may be subject to frequent
updates.  Both of these characteristics render impractical the encoding
and maintenance of a fixed, in-core lexicon.  We have developed and
implemented a technique for reducing the number of lexical ambiguities
for unknown terms by deferring lexical decisions as long as possible,
and using a simple cost model to select an appropriate method for
resolving remaining ambiguities.

\ssect Common expression analysis.

We have shown that common expression analysis can practically be applied
in three different settings for optimization of database request.  The
Query Graph representation of queries, which we originated, is the basis
for this work.  It represents the structure of requests in an intuitively
clear manner.  Also the decomposition into nodes (relation occurrences in
queries labelled with internal selection predicates and projected
attributes) and edges (join predicates) serves as a convenient structure
for automatic analysis in query optimization.

We have written program that detects
whether or not the result of one query can be used to support answering
another query.  A paper describing parts of this work, ``Common
Expression Analysis Using the Query Graph Model'' has been presented by
Shel Finkelstein.  This paper
describes both the query graph, and the first two settings for
optimization described below.

\ni 1. In an interpretive system, answers to previous queries, or temporaries
formed in the process of obtaining them, may significantly reduce
processing time for subsequent queries.  We have defined a methodology,
based on the Query Graph representation, for deciding cheaply whether such
temporaries are helpful.

\ni 2. A transaction which contains multiple queries may perform redundant
database operations.  We have described a procedure for optimization of a
collection of queries, which involves computing least upper bounds on
Query Graph nodes (which correspond to scans through relations which might
profitably be combined).  These are extended to maximal subexpressions
between queries, and a heuristic procedure examines possible query
revisions to find the best execution procedure.

\ni 3. We have extended the concept of optimization of generated code to
languages with embedded queries (such as SQL in PL/I).  We have analyzed
how queries in loops can be optimized differentially.  Also, we have
studied how global flow analysis can be used to determine available
database expressions at places in the program.

\ssect Finite differencing.

We have cooperated in the investigation of the transformational technique 
of finite  differencing for the  specification, implementation, and 
application of derived data in the context of a set-theoretic 
entity-relationship data model.  A framework for the automatic 
maintenance of derived data has been presented.  This framework is 
based on in which repeated costly computations 
are replaced by more efficient incremental counterparts.  Applications 
of this approach are in integrity control and query/transaction optimization.
\ref:Paige.1982.

\ssect File access system.

     A file access system that uses symbolic keys to access variable
length records based in PASCAL and supporting several host languages,
including PASCAL, INTERLISP, and FORTRAN has been developed and is now
being tested.  The services that this system, named FLASH, expects from
the underlying operating system are limited to directory management for
named segments of secondary storage, and access to fixed size blocks or
pages of these segments.  In a multi-user environment some locking
facilities are also needed.  Since this subproject is the basis for 
long-range database system development, reliability and efficiency have 
been major design and implementation objectives.  It is specifically 
designed to provide strong and symmetric support facilities for databases, 
so that powerful database systems can become easier to implement than 
they are using conventional files, designed with only programmer's needs 
in mind.  The underlying structure uses B+ trees for storage of both 
primary and secondary keys \ref:Allchin1980..
This system will be used to study various dynamic storage and 
retrieval strategies.  The experience of implementing FLASH is being 
used to define an Input-Output  package for the ADA language.

\ssect Database machines.

     One focus of research activity within the KBMS project has involved
the design and analysis of alternative hardware machine architectures
oriented toward the very rapid execution of the relational operations
which arise frequently in large-scale database management applications.
During the past year, this research has yielded certain surprising and
potentially important results which may ultimately prove useful in
designing cost-effective, extremely high-performance database machines.

     These results are manifested in a ``high-level'' design for a
specialized non-von Neumann machine, portions of which would be
implemented in VLSI, which would support the highly efficient evaluation
of the most computationally complex operators of a relational algebra,
specifically projection with elimination of duplicate tuples and the
equi-join.  Based on a hierarchy of associative storage devices, this
architecture permits an O(log n) improvement in time complexity over the
best known evaluation methods for these operators on a conventional
computer system, without the use of redundant storage, and using
currently available and potentially competitive technology.  In many
cases of practical import, the proposed architecture should also permit
a very significant improvement (by a factor roughly proportional to the
size of the primary associative storage device) over the performance of
previously implemented or proposed database machine architectures based
on associative secondary storage devices \ref:Shaw.1981..
This work is the basis for further VLSI data-oriented architectural
research in progress at Columbia university.

\ssect Execution-time Maintenance of Distributed Databases.

     The management of redundant, distributed data can seriously affect
system performance.  We have analyzed and developed algorithms for
integrity maintenance.  The use of `hole-lists,' to inform nodes of
update status of transaction while passing a minimal amount of
information, has been shown to be effective.  The analyses has also
shown that it is difficult to better the performance of centralized
control methods, if sufficient backup can be provided in the responsible
nodes \ref:Garcia.1982..

     The separation of read-transactions into three classes, namely
those that require no or minimal consistency, auditable consistency, and
time-critical consistency, can improve aggregate system performance.
The problems arising from serving transactions that support planning
functions, which require access to large granules of the database, can
be greatly reduced by lowering their consistency demands.

\sect Stanford ARPA-related Reports and Papers.

These books, papers and reports document research supported at Stanford by 
ARPA under current and preceding contracts to the investigators collaborating
in this request.

\baselineskip 12pt

\makeref:Allchin.1980.{
Allchin,  J.,  A.  Keller,   and  G.  Wiederhold:  \article{FLASH:  A  Language-
     Independent Portable File Access System}; Proceedings of ACM SIGMOD
     Conference, May 1980, pp. 151--156.}

\makeref:Barr.1980.{Barr,  A.  and  J. Davidson:  
\article{Representation  of  Knowledge};  Stanford
     University CS Report  CS-80-793, March 1980.}

\makeref:Ceri.1983.{
Ceri, Stefano, S. B. Navathe, and Gio Wiederhold:  \article{Distribution
	Design of Logical Database Schemas}; to be published in
	Transactions on Software Engineering.}

\makeref:Davidson.1980.{
Davidson,  J. and  S.J. Kaplan:  \article{Parsing in  the Absence  of a Complete
     Lexicon}; Proceedings of the 18th Annual Meeting of the Association
     for Computational Linguistics, Philadelphia, June 19-22, 1980.}

\makeref:El-Masri.1979a.{
El-Masri,  R. and G.  Wiederhold: \article{Database Model  Integration Using the
     Structural  Model}; Proceedings  of the the  ACM SIGMOD Conference,
     Boston, MA., June 1979, pp 191--198.}

\makeref:El-Masri.1979b.{
El-Masri, R.  and G. Wiederhold: \article{Properties  of Relationships and Their
     Representation}; Proceedings of the 1979 NCC, AFIPS Vol. 49, August
     1979,  pp.   319-326.}

\makeref:El-Masri.1980.{
El-Masri,  R.:  \book{On   the  Design,  Use,  and
     Integration of Data Models;} Ph.D. dissertation, Stanford CS Report
      CS-80-801, June 1980.}

\makeref:El-Masri.1981.{
El-Masri, Ramez and Gio Wiederhold:  \article{Formal Specifications of GORDAS:
	A High-Level Query Language for Graph Databases}; Proceedings
	of the Second International Conference on the Entity-Relationship
	Approach to System Analysis and Design, Washington, D.C., Oct.
	12--14, 1981.}

\makeref:Garcia-Molina.1977.{
Garcia-Molina,  H. and G.  Wiederhold: \article{Application of  the Contract Net
     Protocol to Distributed  Data Bases}; Stanford University Heuristic
     Programming Project paper HPP-77-21, April 1977.}

\makeref:Garcia-Molina.1978a.{
Garcia-Molina, H.:  \article{Distributed Database Coupling}; Stanford University
     Heuristic Programming  Project  paper  HPP-78-4, March  1978,  also
     appears  in the Third USA-Japan  Conference Proceedings, AFIPS, San
     Francisco, October, 1978, pp. 75--79.}

\makeref:Garcia-Molina.1978b.{
Garcia-Molina, H.:  \article{Performance  Comparison  of Update  Algorithms  for
     Distributed  Databases,  Part  I};  Technical  Note  143,  Stanford
     University, Computer  Systems Laboratory, Departments of Electrical
     Engineering and Computer Science, June 1978.}

\makeref:Garcia-Molina.1978c.{
Garcia-Molina,  H.:   \article{Crash  Recovery   in  the   Centralized   Locking
     Algorithm};  Technical   Note  153,  Stanford  University,  Digital
     Systems  Laboratory,  Departments  of  Electrical  Engineering  and
     Computer Science, November 1978.}

\makeref:Garcia-Molina.1978d.{
Garcia-Molina, H.: \article{Performance  Comparison of Two Update Algorithms for
     Distributed Databases}; Proceedings  of the 3rd Berkeley Conference
     on Distributed Data  Management and Computer Networks, August 1978,
     pp.108--119}

\makeref:Garcia-Molina.1978e.{
Garcia-Molina, H.:  \article{Performance  Comparison  of Update  Algorithms  for
     Distributed  Databases,  Part II};  Technical  Note  146,  Stanford
     University, Computer Systems Laboratory, December 1978.}

\makeref:Garcia-Molina.1978f.{
Garcia-Molina, H:  \article{Distributed Database Couplings}; Stanford University
     Heuristic Programming Project paper HPP-78-4, March 1978.}

\makeref:Garcia-Molina.1979a.{
Garcia-Molina,  H.:  \article{Restricted   Update  Transactions  and  Read-Only
     Transactions}; Technical  Note 154,  Stanford University,  Computer
     Systems Laboratory, January 1979.}

\makeref:Garcia-Molina.1979b.{
Garcia-Molina,  H.:   \article{Partitioned  Data,   Multiple  Controllers,   and
     Transactions with  an Initially  Unspecified Base  Set};  Technical
     Note 155, Stanford University, Computer System Laboratory, February
     1979.}

\makeref:Garcia-Molina.1979c.{
Garcia-Molina, H.:  \article{A  Concurrency  Control Mechanism  for  Distributed
     Databases Which  Uses Centralized Locking Controllers}; Proceedings
     of the  4th Berkeley Conference on  Distributed Data Management and
     Computer Networks, August 1979, pp.113--124.}

\makeref:Garcia-Molina.1979d.{
Garcia-Molina,   H.:   \article{Centralized  Control   Update   Algorithms   for
     Distributed  Databases};   Proceedings  of  the  1st  International
     Conference on Distributed Processing Systems, October 1979.}

\makeref:Garcia-Molina.1979e.{
Garcia-Molina, H.: \article{Performance of Update Algorithms for Replicated Data
     in   a   Distributed  Database};   Ph.D.   dissertation,   Stanford
     University, Computer Science Department report CS-79-744, 1979.}

\makeref:Garcia-Molina.1980.{
Garcia-Molina, H. and Wiederhold, G.: \article{Read Only Transactions}; Stanford
     University Computer  Science  Department report   CS-80-797,  April
     1980; ACM TODS, Vol.7 No.2, Jun.1982, pp.209--234.}

\makeref:Garcia-Molina.1981.{
Garcia-Molina, H.: \article{Performance of Update Algorithms for Replicated Data
     in   a   Distributed  Database};   (revised)
     UMI Research Press, Ann Arbor MI, ISBN 0-8357-1219-2, Aug.1981, 320pp.}

\makeref:Ghosh.1979.{
Ghosh, S.,  A.F. Cardenas,  I. Mijares,  and G.  Wiederhold: \article{Some  Very
     Large  Data  Bases  in  Developing  Countries};  5th  International
     Conference on Very Large Databases, Rio de Janeiro, Brazil, October
     1979, pp. 173--182.}

\makeref:Kaplan.1979a.{
Kaplan,  S.J.: \article{Cooperative  Responses from A  Portable Natural Language
     Data   Base  Query  System};  Ph.D.   dissertation,  University  of
     Pennsylvania,   July  1979,  also   Stanford  University  Heuristic
     Programming Project paper HPP-79-19.}

\makeref:Kaplan.1979b.{
Kaplan, S. J.,  E. Mays, and A. K. Joshi:  \article{A Technique for Managing the
     Lexicon in  a Natural Language Interface to  a Changing Data Base};
     proceedings of the 5th International Joint Conference on Artificial
     Intelligence, Tokyo, Japan, August 1979.}

\makeref:Kaplan.1980.{
Kaplan,  S. J.:  \article{Appropriate Responses to  Inappropriate Questions}; to
     appear in \book{Formal Aspects  of Language and Discourse}, A. K. Joshi,
     I. A. Sag. and B. L. Webber, Eds., Cambridge University Press, 1980.}

\makeref:Keller.1981.{
Keller, Arthur M. and Gio Wiederhold:  \article{Validation of Updates Against
	the Structural Database Model}; Symposium on Reliability in
	Distributed Software and Database Systems, July 1981,
	Pittsburgh, PA., pp.195--199.}

\makeref:Keller.1982.{
Keller, Arthur M. and Gio Wiederhold:  \article{Updates to Relational Databases
	through Views Involving Joins}; 2nd International Conference
	on Databases:  Improving Usability and Responsiveness, Jerusalem,
	Israel, Academic Press, June 1982, pp. 363--384.}

\makeref:King.1979.{
King,  J.: \article{Exploring the  Use of Domain Knowledge  for Query Processing
     Efficiency};  Stanford  University  Heuristic  Programming  Project
     paper  HPP-79-30, December, 1979.}

\makeref:King.1980a.{
King, J.: \article{Modelling Concepts  for Reasoning about Access to Knowledge};
     proceedings  of the ACM  Workshop on Data  Abstraction, Data Bases,
     and Conceptual Modelling, Pingree Park, Co., June 23--26, 1980.}

\makeref:King.1980b.{
King, J.:  \article{Intelligent Retrieval  Planning}; Proceedings  of the  first
     National  Conference  on Artificial  Intelligence,  Stanford,  CA.,
     August 1980, pp. 243--245.}

\makeref:Martin.1977.{
Martin, N.,  P. Friedland,  J. King,  and M.J.  Stefik: \article{Knowledge  Base
     Management for Experiment Planning}; Stanford University, Heuristic
     Programming Project paper HPP-77-19 Report, August 1977.}

\makeref:Minoura.1981.{
Minoura, Toshimi and Gio Wiederhold: \article{Resilient Extended True-Copy
	Token Scheme for a Distributed Database System}; Symposium
	on Reliability in Distributed Software and Database Systems,
	July 1981, Pittsburgh, PA., pp.1--12.}

\makeref:Minoura.1982.{
Minoura, Toshimi and Gio Wiederhold: \article{Resilient Extended True-Copy
	Token Scheme for a Distributed Database System}; IEEE
	Transactions on Software Engineering, Vol. SE-8, No. 3,
	May 1982, pp. 173--188.}

\makeref:Paige.1982.{
Paige, Robert,
\article{Applications of Finite Differencing to Database Integrity Control and Query/Transaction Optimization};
 in Bases Logiques pour Bases de Donnees, Nicolas (Ed.), Onera-Cert, Toulouse, 1982.}

\makeref:Shaw.1979.{
Shaw, D.:  \article{A  Hierarchical Associative  Architecture for  the  Parallel
     Evaluation  of Relational Algebraic  Database Primitives}; Stanford
     Computer Science Department Report CS-79-778, October 1979.}

\makeref:Shaw.1980a.{
Shaw,  D.: \article{A Relational Database  Machine Architecture}; Proceedings of
     the   1980  Workshop  on  Computer   Architecture  for  Non-Numeric
     Processing, Asilomar,  CA, March, 1980, also SIGMOD  vol. X, no. 4,
     and SIGIR vol XV, no. 2, April 1980, pp.84--95.}

\makeref:Shaw.1980b.{
Shaw, D.: \article{Knowledge-Based Retrieval on a Relational Databased Machine};
     PhD Dissertation,  Stanford University, Computer Science Department
     report CS-80-823, September, 1980.}

\makeref:Whang.1981.{
Whang, K., Wiederhold, G., and Sagalowicz, S.: \article{Separability: An
approach to Physical Database Design}; Proc. Seventh
International Conference on Very Large Data Bases, 
Zaniolo and Delobel(eds.), Cannes, Frances, Sep.1981, pp.320--332.}

\makeref:Whang.1982.{
Whang,K.-Y., Wiederhold,G., and Sagalowicz,D.:
\article{Physical Design of Network Model Databases Using the Property of 
Separability}; 
in Eighth International Conference on Very Large Data Bases, 
McLeod and Villasenor (eds.), Mexico City, Sep.1982, pp.98--107.}

\makeref:Wiederhold.1978a.{
Wiederhold, G.:   \article{Introducing  Semantic  Information   into  a  Database
     Schema}; Proceedings of  the CIPS Session '78, Canadian Information
     Processing Society, September, 1978, pp. 338--391.}

\makeref:Wiederhold.1978b.{
Wiederhold, G.: \article{Management of Semantic Information for Databases}; HPP-78-12,
     Proceedings of the 3rd USA-Japan Conference, Session 10-2-1,
     San Francisco, October 1978.}

\makeref:Wiederhold.1979a.{
Wiederhold, G. and R. El-Masri: \article{Structural Model for Database Systems};
     Stanford University,  Computer Science Department report CS-79-722,
     April 1979.}

\makeref:Wiederhold.1979b.{
Wiederhold, G.  and  R. El-Masri:  \article{The  Structural Model  for  Database
     Design}; Proceedings  of the  International Conference  on  
Entity-Relationship Approach to Systems Analysis and Design, North Holland
     Press, December 1979, pp 247--267.}

\makeref:Wiederhold.1979c.{
Wiederhold,  G.: \article{Databases for Economic  Planning in India}; Management
     Sciences and the Development of Asian Economies, S. Torok (editor),
     Times Books International, Singapore, 1979.}

\makeref:Wiederhold.1980a.{
Wiederhold,  G.: \article{Databases  in  Health  Care;}
     Stanford CS Report 80-790, March 1980.}

\makeref:Wiederhold.1980b.{
Wiederhold,  G.,  Beetem,  A.,  Short, G.:  \article{A  Database  Approach  to
     Communication  in  VLSI   Design};  TR  196,  Stanford  University,
     Computer Systems Laboratory, 1980.}

\makeref:Wiederhold.1980c.{
Wiederhold, Gio:  \article{New Technologies}; in \book{The Computer in the Doctor's Office},
	O. Rienhoff/M.E. Abrams (Eds.), North-Holland Publishing Company,
	IFIP, 1980, pp. 263--264.}

\makeref:Wiederhold.1980d.{
Wiederhold,G. (Translator R. Gritsch);
\article{Datenbanken, Analyse---Design---Erfahrungen};	 Band 1 Dateisysteme
R.Oldenbourg Verlag M\"unchen 1980, Reihe Datenverarbeitung, 454 pp.}

\makeref:Wiederhold.1981a.{
Wiederhold,G.
\article{Databases for Health Care};
 Lecture Notes in Medical Informatics, No.12, Lindberge and Reichertz,(eds.),
  Springer-Verlag, Berlin, Heidelberg, New York, 1981, 75 pp.}

\makeref:Wiederhold.1981b.{
Wiederhold, G:  \article{Database Technology in Healthcare};
Journal of Medical Systems, Plenum, Vol.5, No.3, Sept. 1981, pp. 175--196.}

\makeref:Wiederhold.1981c.{
Wiederhold, G., and Minoura, T.: \article{Resilient Extended True Copy Scheme
for Distributed Database Systems}; IEEE Symposium on Reliability in
Distributed Software and Database Systems, March, 1981.}

\makeref:Wiederhold.1981d.{
Wiederhold,G., Kaplan,J., and Sagalowicz,D.;
\article{Research in Knowledge Base Management Systems};
 ACM SIGMOD Record, Vol.11 No.3, Apr.1981, pp.26--54.}

\makeref:Wiederhold.1982a.{
Wiederhold, Gio, Anne Beetem, and Garret Short:  \article{A Database Approach
        to Communication in VLSI Design}; IEEE Transactions on Design
        Automation, Vol. CAD-1, No. 2, April 1982, pp. 57--63.}

\makeref:Wiederhold.1982b.{
Wiederhold, Gio: \article{A Method for the Design of Multi-Objective Databases};
        Proceedings of the Annual Meeting of the American Society of
	Mechanical Engineers, June 1982, pp. 161--165.}

\makeref:Wiederhold.1982c.{
Wiederhold,G.(ed.):
 \article{Second Symp. on Reliability in Distributed Software and Database Systems};
IEEE Pub. No.82CH1792-1, 1982.}

\makeref:Wiederhold.1982d.{
Wiederhold, Gio:  \article{Applications of Computers in Medicine}; Encyclopedia
	of Computer Science, A. Ralston (editor), 
        Second edition; van Norstrand-Reinhold 1982, pp.686-688, 934-940.}

\makeref:Wiederhold.1982e.{
Wiederhold, Gio:  \article{Scientific Computing:  A Scientific Group of Mixed
	Background Attempts to Cope with a Broad Spectrum of Problems}:
	abstracted in Roles of Industry and the University in Computer
	Research and Development, National Academy Press, Washington,
	D.C. 1982, pp. 60--66.}

\makeref:Wiederhold.1983.{
Wiederhold, Gio:  \book{Database Design}; (in the Computer Science Series)
        Second edition, Jan. 1983, 768 pp.}

\makeref:Whang.1983.{
Whang,K-Y., Wiederhold,G., and Sagalowicz,D.:
\article{Estimating Block Accesses in Database Organizations---A Closed,
  Non-iterative Formula }; to be published in Communications of the ACM, 1983.}

\baselineskip 15pt
\vfill\eject
\sect Transfer to DOD.

The primary means of transfer of our results to the various branches of
the DOD will be in the form of published papers, conference
presentations, invited talks, and briefings. During the current KBMS
contract, numerous papers were presented, published, and disseminated
through the normal channels for academic research. (A bibliography is
enclosed in the ``previous work'' section.) Contact has been maintained
with local industry through a weekly seminar. Regular outside
participants in these seminars include staff from Control Data Corp.,
IBM, Lockheed, Hewlett-Packard, SRI International, Xerox, Honeywell,
Tandem, Science Applications Inc., and System Control Inc.  In addition,
special presentations were given to various visitors, usually at the
request of DARPA or NAVALEX.  Special contact was maintained with the
Defense Mapping Agency, where information management problems are
particularly relevant. We anticipate similar activities to continue
under the current proposal.

The work will mainly take the form of PhD level research, to be
performed by Stanford PhD students under the direction of the
investigators named in the proposal. The results will be primarily in
the form of completed PhD dissertations, formal and informal technical
publications, and demonstration implementations when appropriate. The
work will be disseminated to researchers and practitioners in the fields
of database management, distributed systems, and applied Artificial
Intelligence. Students who have participated in the KBMS project can now
be found at a number of important industrial and academic sites.

\sect Relevance to agency objectives.

The proposed research complements other currently supported efforts in
the Stanford Computer Science Department as well as other research
institutions, and considerable interaction with these projects is
anticipated.

The newly initiated Stanford ``Intelligent Agents'' project, funded by
DARPA, is concerned with the development of Artificial Intelligence
techniques for facilitating a user's interaction with a distributed,
heterogeneous computing environment. The primary areas of investigation
are the problems of inducing user's intentions, distributed problem
solving with error recovery, planning with incomplete knowledge, and
high-level communication between dissimilar processors. While these
areas are disjoint with the subject matter of the present proposal,
there are some deeper similarities. Specifically, both projects will be
oriented toward the problems of management and control of distributed
computing environments, though from different perspectives. While the
Intelligent Agents project will develop novel AI knowledge
representation and deduction techniques for multiple computers and
systems, the current proposal will deal with the specifics of 
formal and heuristic information management in that same environment.

Previously, the KBMS project has benefited from the advice and help of
the Defense Mapping Agency, who kindly supplied us with non-classified
information regarding ships, ports, and cargoes. From this information,
we were able to populate a realistic simulated database of considerable
complexity, to serve as a practical testbed for our ideas. We anticipate
continued interaction with the DMA.

\vfill\eject
\sect Reports and Papers.
\baselineskip 12pt

\makeref:Bachman.1972.{
C. W. Bachman, \article{The Evolution of Storage Structures};  CACM
     Vol. 15, Num. 7, July 1972, pp. 628--634.}

\makeref:Blasgen.1977.{
M. Blasgen, K. Eswaren,
\article{Storage and Access in Relational Data Bases};
IBM Sys. J., Vol. 16, No. 4, 1977.}

\makeref:Bleier.1967.{
R. E. Bleier, \article{Treating Hierarchical Data Structures in  the
     SDC Time-shared  Data Management  System  (TDMS)}; Proc.  22nd  ACM
     National Conference 1967, MDI Pub. Wayne, Pa., pp.41--49}

\makeref:Boyce.1975.{
R. Boyce, D. Chamberlin, M.  Hammer and W. King,  \article{Specifying
     queries as relational  expressions: the  SQUARE Data  Sublanguage};
     CACM, Vol. 18, No. 11, Nov. 1975, pp.621--628.}

\makeref:Burkhard.1976.{
W. A. Burkhard, \article{Hashing  and Trie Algorithms for  Partial
     Match Retrieval}; TODS Vol. 1, Num. 2, June 1976, pp. 175--187.}

\makeref:Chamberlin.1974.{
D. D. Chamberlin and R. F. Boyce, \article{SEQUEL: a  Structured
     English  Query  Language};  Proc.  ACM  SIGMOD  workshop  on   Data
     Description, Access and Control, May 1974, pp.249--264.}

\makeref:Chang.1976.{
C.  L.  Chang,  \article{DEDUCE:  a  Deductive  Query  Language   for
     Relational Data  Bases};  in: \book{Pattern  Recognition  and  Artificial
     Intelligence}, Academic Press, 1976, pp.108--134.}

\makeref:Chang.1976.{
S. Chang, M. O'Brien, J. Read, A. Borovec, W. Cheng,and  J.
     S. Ke, \article{Design Considerations of a  Data Base System in a  Clinical
     Network Environment}; Proc. 1976 NCC, AFIPS, Vol. 45, pp.277--286.}

\makeref:CODASYL.1971.{
\article{Data  Base Task  Group  of CODASYL  Programming  Language
     Committee}; ACM report, Apr. 1971}

\makeref:CODASYL.1974.{
\article{CODASYL Data Description Language,  Journal of Development
     June 73}; NBS Handbook 113, Government Printing Office, Washington,
     D.C., January 1974, 155pp.}

\makeref:Codd.1970.{
E. F. Codd, \article{A Relational Model of Data for Large Shared  Data
     Banks}; CACM Vol. 13, Num. 6, June 1970, pp. 377--387.}

\makeref:Codd.1971.{
E. F. Codd, \article{A Data Base Sublanguage Founded on the Relational
     Calculus}; Proc. ACM SIGFIDET workshop on Data Description,  Access
     and Control, San Diego, Nov. 1971, pp. 35--68.}

\makeref:Codd.1974.{
E. F. Codd, \article{Seven Steps to Rendezvous with the Casual  User};
     in: \book{Data Base Management}, J. W.  Klimbie and K. I. Koffeman,  eds.,
     North Holland, 1974, pp.179--200.}

\makeref:Cohen.1974.{
S. N. Cohen  et. al., \article{Computer  Monitoring and Reporting  of
     Drug  Interactions};  Proc.  MEDINFO   1974,  IFIP,  Anderson   and
     Forsythe, Editors, Congress, North Holland 1974.}

\makeref:Duda.1978.{
R. O. Duda, P. E. Hart, P. Barrett, J. G. Gaschnig, K.
Konolidge, R. Reboh, and J. Slocum, \article{Development of the Prospector
Consultation system for mineral exploration}; Final Report, SRI
project 5821 and 6415, October 1978.}

\makeref:Everest.1974.{
G. C. Everest,  \article{The Objectives of  Data Base  Management};
     Proc. 4th  International  Symposium  on  Computer  and  Information
     Sciences, Plenum Press, 1974, pp. 1--35.}

\makeref:Garcia.1977.{
H. Garcia-Molina, \article{Overview and Bibliography of  Distributed
     Databases}; Computer Science Dept., Stanford University}

\makeref:Garcia.1983.{
H.  Garcia-Molina,   \article{Distributed   Database   Coupling};   in
     preparation}

\makeref:Germano.198?.{
F.  Germano,  Ph.D.  thesis,  in  progress,  Wharton  School,
     University of Pennsylvania}

\makeref:Ghosh.1975.{
S. P.  Ghosh, \article{Consecutive  Storage  of Relevant  Records  with
     Redundancy}; CACM Vol. 16, Num. 8, August 1975, pp. 464--471.}

\makeref:Grosz.1977a.{
B. J. Grosz, \article{The Representation and Use of Focus in  Dialog
     Understanding}; Ph.  D. Thesis,  The  University of  California  at
     Berkeley, June 1977.}

\makeref:Grosz.1977b.{
B. J.  Grosz, \article{The  Representation  and Use  of Focus  in  a
     System for  Understanding  Dialogs}; Proc.  5th  IJCAI,  Cambridge,
     Mass., 1977, Vol. 1, pp. 67--76.}

\makeref:Hammer.1976.{
M. M. Hammer, A. Chan,
\article{Index Selection in a Self-Adaptive Database Management System};
Proc. ACM-SIGMOD Conf., Washington D.C., June 1976, pp.1--8.}

\makeref:Hammer.1977.{
M. M. Hammer, 
\article{Self-Adaptive Automatic Data Base Design};
Proc. AFIPS 1977 NCC, pp.123--129.}

\makeref:Hammer.1978.{
M. M. Hammer and D. McLeod, \article{The Semantic Data Model, a
Modelling Mechanism for Database Applications}; in E. Lowenthal and
N. B. Dale (eds.), ACM SIGMOD Intl. Conf. on Management of Data,
Austin, Texas, 1978, pp. 26--36.}

\makeref:Hammer.1980.{
M. M. Hammer and D. Shipman, \article{Reliability Mechanisms for
SDD-1}; Transactions on Database Systems 5, number 4, December, 1980,
pp. 431--466.}

\makeref:Harris.1977.{
L. R. Harris,  \article{ROBOT: a High  Performance Natural  Language
     Processor for Data  Base Query};  SIGART Newsletter,  No. 61,  Feb.
     1977, pp. 39--40.}

\makeref:Held.1976.{
G. D.  Held,  M.  R.  Stonebraker  and  E.  Wong,  \article{INGRES:  a
     Relational  Data Base System};  AFIPS Conf. Proc.,  vol. 44,  1975,
     pp. 416}

\makeref:Hendrix.1975.{
G. G. Hendrix, \article{Expanding the Utility of Semantic  Networks
     through Partitioning}; SRI Artificial Intelligence Group  Technical
     Note 105, June 1975.}

\makeref:Hendrix.1977.{
G. G.  Hendrix,  \article{Human  Engineering  for  Applied  Natural
     Language Processing};  Proc.  5th IJCAI,  Cambridge,  Mass.,  1977,
     vol.1, pp. 183--191.}

\makeref:Kaplan.1973.{
K.  R.  Kaplan  and  R.  O.  Winder,  \article{Cache-based  Computer
     Systems}; Computer, March 1973, pp. 31--36.}

\makeref:Kaplan.1979.{
S. J. Kaplan, \article{Cooperative Responses from a Portable Natural
     Language Data Base Query System}; Ph.D. dissertation,  Dept. of Computer 
     and Information Science, University of Pennsylvania, Philadelphia, Pa., 
     1979.}

\makeref:Lee.1978.{
Lee, R. M., \article{Conversational Aspects of Database Interactions};
     proceedings of the International Conference on Very Large Data Bases, 
     Berlin, Germany, 1978.}

\makeref:Lehnert.1977.{
W. Lehnert, \article{Human and Computational Question Answering};
     in Cognitive Science Vol.  1, 1, 1977.}

\makeref:Lucas.1975.{
H. C. Lucas, \article{Performance and Use of an Information  System};
     Management Science, Vol. 21, No.8, April 1975, pp.908--919}

\makeref:Marill.1975.{
T. Marill and  D. Stern, \article{The  Datacomputer, A Network  Data
     Utility}; Proc. 1975 NCC, AFIPS, Vol. 44, pp. 389--395.}

\makeref:McDermott.1975.{
D. V. McDermott, \article{Very  Large  Planner---type  Data Bases};
     M.I.T. Artificial Intelligence Laboratory Memo 339, September 1975.}

\makeref:Montgomery.1972.{
C. A.  Montgomery,  \article{Is Natural  Language  an  Unnatural
     Query Language}; Proc. 27th Nat. Conf., ACM, 1972, pp. 1075--1078.}

\makeref:Moore.1978.{
B. C. Moore, \article{Handling Complex Queries in a Distributed Data 
     Base}; Technical Report, Artificial Intelligence Center, SRI 
     International, 1978.}

\makeref:Mylopoulos.1975.{
J.  Mylopoulos  and  N.  Roussopoulos,  \article{Using  Semantic
     Networks for Data  Base Management}; Proc.  International Conf.  on
     Very  Large  Data  Bases,  Framingham,  Massachusetts,  Sept. 1975,
     pp. 144--172.}

\makeref:Novak.1976.{
G. S.  Novak,  \article{Computer Understanding  of  Physics  Problems
     Stated in  Natural  Language}; American  Journal  of  Computational
     Linguistics, Microfiche 53, 1976.}

\makeref:Petrick.1976.{
S.  R.  Petrick,  \article{On   Natural  Language  Based   Computer
     Systems}; IBM Journal of Research and Development, vol.20, no.4, July
     1976, pp. 314--125}

\makeref:Rivest.1976.{
R.  L.   Rivest,  \article{On   Self---Organizing  Sequential   Search
     Heuristics}; CACM, Vol. 19, Num. 2, February 1976, pp. 63--67.}

\makeref:Roussopoulos.1977.{
N.  Roussopoulos,   \article{A  Semantic   Network  Model   of
     Databases}; PhD  Thesis,  Computer  Science  Dept.,  University  of
     Toronto, 1977.}

\makeref:Sacerdoti.1977a.{
E. D. Sacerdoti,  \article{Language Access  to Distributed  Data
     With Error Recovery}; Proc. 5th International Joint Conference	
     on Artificial Intelligence, Cambridge, Massachusetts, (August 1977).}

\makeref:Sacerdoti.1977b.{
E. D. Sacerdoti, \book{A  Structure for Plans and  Behavior};
     Elsevier North-Holland, 1977.}

\makeref:Sagalowicz.1977.{
D.  Sagalowicz,   \article{IDA:  An   Intelligent  Data   Access
     Program}; Proc. Third International Conference on Very Large	
     Data Bases, Tokyo, Japan (October 1977).				}

\makeref:Schkolnick.1977.{
M. Schkolnick, \article{A Clustering Algorithm for  Hierarchical
     Structures}; ACM--TODS, Vol. 2, Num. 1, March 1977, pp.27-44.}

\makeref:Selinger.1979.{
P. Selinger et al., \article{Access Path Selection in a Relational
Database Management System}; IBM technical report RJ2429, 1979.}

\makeref:Shneiderman.1973.{
B.  Shneiderman,  \article{Optimum  Data  Base   Reorganization
     Points}; Comm. ACM, vol.16, no.6, June 1973, pp. 362--365}

\makeref:Shortliffe.1973.{
E. Shortliffe,  S.  G. Axline,  B.  G. Buchanan,  T.  C.
     Merigan and S.  N. Cohen,  \article{An Artificial  Intelligence Program  to
     Advise  Physicians  Regarding  Antimicrobial  Therapy};  Comp.  and
     Biomed. Res., Vol. 6, Num. 6, December 1973, pp.544--560.}

\makeref:Sibley.1976.{
E.  H.  Sibley  and  J.  P.  Fry,  \article{Evolution  of  Data---Base
     Management Systems}; ACM Computing Surveys,  Vol. 8, Num. 1,  March
     1976, pp. 7--42}

\makeref:Sowa.1976.{
J. F. Sowa,  \article{Conceptual Graphs for  a Data Base  Interface};
     IBM Journal of Research and Development, Vol. 20, No. 4, July 1976,
     pp. 336--357.}

\makeref:Steel.1974.{
T. B.  Steel  Jr.,  \article{Data Base  Systems---Implications  for
     Commerce and Industry};  in: \book{Data  Base Management  Systems}, D.  A.
     Jardine, editor, North Holland 1974.}

\makeref:Steel.1975.{
T. B.  Steel Jr.,  \article{ANSI/X3/SPARC Study  Group on  Data  Base
     Management   Systems,   Interim   Report   75-02-08};   FDT   (Pub.
     ACM-SIGMOD), Vol. 7, Num. 2, 1975.}

\makeref:Stocker.1977.{
P. M. Stocker,
\article{The Structuring of Data Bases at the Implementation Level};
in \book{Architecture and Models in Data Base Management Systems}, Nijssen (ed.),
North Holland, 1977, pp.261--276.}

\makeref:Taylor.1974.{
R. W. Taylor, \article{When Are Pointer Arrays Better Than  Chains};
     Proc. 1974 ACM Nat. Conf., November 1974.}

\makeref:Thompson.1975.{
F. B.  Thompson and  B.  H. Thompson,  \article{Practical  Natural
     Language Processing: the REL System as Prototype}; in: \book{Advances  in
     Computers 13}, M. Rubinoff and  M. C. Yovits, eds., Academic  Press,
     1975, pp. 109--168.}

\makeref:Tuel.1978.{
W. G. Tuel, \article{Reorganization Points for Linearly Growing Files};
ACM TODS, Vol. 3, No. 1, Sept. 1978, pp.32--40.
}

\makeref:Walker.1977.{
D. E. Walker  et al., \article{An  Overview of Speech  Understanding
     Research at  SRI};  Proc.  5th International  Joint  Conference  on
     Artificial Intelligence, Cambridge, Mass., Aug. 1977.}

\makeref:Waltz.1975.{
D. L. Waltz,  \article{Natural Language Access  to a Large  Database:
     An Engineering  Approach}; Adv.  Papers 4th  Intl. Joint  Conf.  on
     Artificial Intelligence,  Tbilisi,  U.S.S.R., September  1975,  pp.
     868--872.}

\makeref:Wiederhold.1975.{
G. Wiederhold,  J. F.  Fries  and S.  Weyl,  \article{Structured
     Organization of Clinical  Data Bases}; Proc.  1975 NCC, AFIPS  Vol.
     44, pp. 479--486.}

\makeref:Wiederhold.1977a.{
G. Wiederhold,  \book{Database Design};  McGraw-Hill,  1977,
     Chapter 7.}

\makeref:Wiederhold.1977b.{
G. Wiederhold, \article{Binding in Information Processing};  in
     preparation.}

\makeref:Wiederhold.1978.{
G. Wiederhold and  R. El-Masri, \article{A  Structural Model  for
     Database Systems}; submitted for publication}

\makeref:Woods.1973.{
W. A. Woods, \article{Progress in Natural Language Understanding,  An
     Application to Lunar Geology}; Proc. 1973 NCC, AFIPS, Vol. 42,  pp.
441--450. }

\makeref:Yao.1976.{
S. B. Yao, K. S. Das, and  T.J. Teory, \article{A Dynamic Database Reorganization Algorithm};
ACM TODS, Vol. 1, No. 2, June 1976, pp.159--174.}

\makeref:Yao.1978.{
S. B, Yao, D. DeJong,
\article{Evaluation of Database Access Paths};
Proc. ACM-SIGMOD Conf., Austin, Texas, May--June 1978, pp.66--77.}

\makeref:Yao.1979.{
S. B. Yao, \article{Optimization of Query Evaluation Algorithms};
ACM TODS, to appear.}

\makeref:Zloof.1975.{
M. Zloof, \article{Query by Example}; AFIPS Conf. Proc., Vol 44, 1975,
     pp.431--438.}

\vfill\eject
%Programming Analysis and Verification
\ctrline{RESEARCH AND DEVELOPMENT}
\ctrline{IN}
\ctrline{ADVANCED PROGRAMMING ENVIRONMENTS}

$$\vcenter{\halign{\lft{#}\cr
David C. Luckham, Professor of Electrical Engineering (Research)\cr
Computer Systems Lab\cr
Electrical Engineering Department\cr
Stanford University\cr}}$$
 
\initsect

\sect Introduction.
\save5\hbox{\count0}

Software engineering is concerned with providing languages, techniques, and
tools that enable programmers to produce reliable high quality software
efficiently.  It addresses the widely recognized problems of systems being
too costly to produce and unreliable in operation.  Software engineering
is developing a new technology for coping with these problems within
the context of the increasing complexity of modern systems.  This
complexity increase, together with a greater demand for new systems than
ever before and a general shortage of skilled personnel, is having the
effect of magnifying the cost, reliability, and quality problems.  The
situation has now reached a point where it is often referred to as ``the
software crisis.''

The major goal of recent research in Software Engineering is to apply
automated techniques to all stages of the software life cycle:
requirements, specification, implementation, and maintenance. This
direction results from a general acceptance that the most promising
approach to solving the software crisis is the development and adoption of
advanced knowledge-based software tools.  Therefore much recent research
effort has focused on three basic areas:

\numitem{(1)}Languages: development of
new machine-processable languages for support of systems production
activities other than implementation (e.g.  formal requirements,
specification, and documentation languages), 

\numitem{(2)}Programming Environments:
the design and implementation of tools based on the new languages for the
support of systems production and the integration of sets of tools into
programming environments, and 

\numitem{(3)}Methodology: development of new
methodology of software production utilizing advanced automated tools and
emphasizing such factors as reliability and reuseability.  

Of particular concern within each of these three areas are the problems
posed by new complex systems that utilize concurrent and distributed
processing.  

The Program Analysis and Verification Group is conducting
research in all three basic areas.  The following two sections discuss (a)
future research directions within the three basic areas, and (b) some of
the recent achievements of the Program Analysis and Verification Group in
these areas.

\sect Research Directions in Advanced Programming Environments.

Advanced Programming Environments integrate sets of programming tools to
provide automated aid at all stages in the production and maintenance of
reliable high quality systems.

Advanced programming environments are intended to support systems
development throughout the systems life cycle.  They integrate tools not
only for compilation and execution of programs, but also various tools
that assist in creation and maintenance.  Examples of such tools are
``smart'' editors, runtime performance analyzers, validation and
verification tools, test case generators, tools for rapid prototyping and
automatic documentation, and project management tools.  An advanced
environment not only makes available a variety of sophisticated software
tools, but also integrates them: the tools interface smoothly, utilizing a
single user interface command language; information generated by one tool
is supplied automatically to other tools; knowledge-based techniques are
employed not only in the individual tools themselves but also in the
environment, e.g., to prompt the timely and correct use of each tool.

The major goals of advanced programming environments are increased
productivity of programmers, the production and maintenance of systems
at lower cost, and production of high quality
systems with demonstrated improvement in reliability and  other
performance criteria.

A new technology for design and construction of many of the new and
sophisticated software tools and a methodology for their use
still need to be developed. Techniques for integration of tools into
coherent environments must also be researched. The following sections
summarize our main research directions.

\ssect Broad Spectrum Languages.

Increasingly, formal methods are being applied to
program development.  Such methods include (a) analysis of requirements,
designs, and implementations for consistency, (b) analysis of runtime
behavior, (c) analysis of communication behavior of concurrent and
distributed systems, and (d) systematic program development by
transformations.  This new programming methodology must be based on new
languages for expressing specification of systems requirements and system
designs, documentation and annotation.  These languages are not
programming languages in themselves, but may be extensions of existing
programming languages.  They are essentially broad-spectrum languages
capable of expressing computational procedures and information associated
with computations (e.g., explanatory information about how a computation
behaves and why it is correct) in a machine processable form.  Their
development may lead to new very high level programming languages.

The languages must be machine-processable.  Methods based on their use in
automated programming environments will facilitate such activities as
rapid prototyping and simulation, systematic testing and error detection,
verification and validation, maintenance, and library classification of
systems packages.  Thus a pressing research direction is the development
of broad-spectrum languages that permit users to express requirements,
specifications, design decisions, and implementation within one unified
linguistic framework.  We are proposing research on broad spectrum
languages.

\ssect Systems Development Methodology.

Programming environments are to support new systems development methods at
all stages of the systems life-cycle leading to a very reliable high
quality end product.  Research to develop new methodology will be
undertaken.  The methodology, based on broad spectrum languages, will
involve formal representation of requirements, very high level formal
specification methods, program transformations at the level of programming
language, and interface transformations between life-cycle stages, i.e.,
transformations from formal requirements to specifications, and from
specifications to various code levels and architectures.

An area of particular concern will be the methodology for developing
distributed and concurrent systems.

\ssect Advanced Programming Environment Tools.

Research into the design and construction of advanced tools automating
systems development methodology based on broad spectrum languages will be
undertaken. Such tools will automate much of the routine work involved
in systems design and development activities. Examples include
support for formalization of requirements,  support for development of
very high level specifications for systems (including linguistic
correctness analysis, symbolic interpretation, consistency analysis),
automation of transformational techniques, validation tools, and
formal verification tools.

\ssect Knowledge-Based Methods and Tools.

Advanced tools and methods in programming environments require strong
capabilities for automated deduction.  Such capabilities represent the
degree to which ``intelligence'' is built into a tool.  The techniques
need to be developed further to the point where machine-assisted reasoning
about programs and programming is no longer practiced by just a few
specialists, but can be introduced into general programming practice.  A
related area for research towards future programming methods and tools is
codification and formalization of programming knowledge and development of
associated techniques for applying this knowledge to systematic program
development.  This research is the foundation for design and
implementation of knowledge-based tools for assisting programmers in
software production.

\ssect Environment User Interface.

Modern user interfaces of programming environments make heavy use of displays
and visual feedback.  These interfaces need to be improved by development of
graphical languages, structure-based editors, and knowledge-based management
facilities. Research in user interfaces will be undertaken.

\ssect Specialized Applications of Broad Spectrum Languages.

Many of the languages, techniques, and tools for specification, design and
analysis of software have special applications in other areas which will
be researched.

One example is the application to early stages of hardware design. There
is no inherent distinction between the design specifications of software
or hardware systems.  Languages and methods that were originally developed
for software can be extended and adapted to simulation and design of
hardware.  Research in this direction can be expected to benefit both
hardware and sofware technology.  Research in specialized applications of
broad spectrum languages will be undertaken.

\sect Recent Accomplishments.

The Program Analysis and Verification Group has designed and implemented
the Stanford Pascal Verifier.  This system is still one of the most
powerful tools for automated and interactive formal verification of
annotated Pascal programs.  The theorem prover component of the verifier
incorporates novel technology for efficient decision procedures.  The
verifier has been used extensively as a teaching tool and in comprehensive
case studies, including the verification of a Pascal compiler; it has been
widely distributed to educational and research institutions.  A special
version of the verifier supports automatic analysis of programs for common
runtime errors.

More recently, the interests of the group have been broadened to include
language design and implementation, the study of distributed and
concurrent systems, and the design and implementation of tools for
advanced programming environments, including analysis tools that
complement verifiers.  Most recent accomplishments in these areas include
the following:

\ni 1. {\bf Adam Compiler effort.}  The Adam compiler supports a very large
subset of Ada including most of the tasking. It was developed to study
techniques of implementing tasking; it is the first compiler to use the
efficient Habermann-Nassi implementation.  Adam was demonstrated at the
Ada symposium in Boston, December 1980.  Currently it is being updated to
support the Ada82 redesign, and is being distributed to commercial and
academic organizations by the Stanford Software Distribution Center.
Reports, user manuals, and publications concerning Adam are available
\ref:Luckham.1981a. \ref:Luckham.1983a. \ref:Luckham.1983b..

\ni 2. {\bf Ada task supervisor packages.}  Ada runtime task supervisor packages
have been designed, implemented in Ada, and compiled using Adam. They form
part of the Adam standard environment. The purpose is to develop a
standard package design for the Ada runtime support. As a consequence:
{\sl (i)} a standard interface between compilers and runtime supervisors
is defined, facilitating portability of compilers, and {\sl (ii)} clearly
defined encapsulation of machine-dependent parts of the supervisor
implementation using Ada package structures facilitates reimplementation
for differing machine architectures.  Task supervisor packages are being
distributed. Reports and publications on supervisor design and
implementation are available \ref:Luckham.1981a. \ref:Falis.1982..

\ni 3. {\bf Anna Language Design.}  Anna is a specification and annotation
language for Ada programs.  It is an extension of Ada that introduces
languages features for formally specifying the intended behavior of Ada
programs (or fragments of programs) at all stages of program design and
development.  Anna annotations are intended to be processable by future
automated tools to aid program design, testing, and maintenance.
Semantics of annotations are defined in terms of Ada concepts thus
simplifying the training of Ada programmers to use Anna to produce machine
processable specifications and documentation.

Anna is a very general formal specification language design;
subsets of Anna are applicable to other Algol-like languages such as
Pascal, PL-1, Concurrent Pascal, and Modula.
The preliminary design includes all Ada constructs except tasking.

An early design for Anna is described in \ref:Krieg-Brueckner $\&$ Luckham.1980..
A preliminary Anna reference manual is available and has been distributed
widely for comment and feedback prior to a final design effort
\ref:Krieg-Brueckner et al.1982c..

\ni 4. {\bf Ada display-oriented structure-based editor.}
A display-oriented structure-based editor has been designed and implemented.
It is language independent; a version supporting Ada is available.
This editor is intended to provide the user interface
for an advanced programming environment.
It has many other applications, e.g. it provides the central facility
for automated teaching courses for programming languages such as Ada.
A user manual is available \ref:Finlayson.1982..
The editor is currently being used for instruction in Ada courses.

\ni 5. {\bf Runtime Monitor for deadness errors in parallel processing.}
Deadness errors result from failure in communication between
the threads of control in a parallel or distributed systems.
They occur unpredictably, sometimes as a result of changes in the
environment external to the program such as runtime scheduling or
I/O processing. They are therefore very difficult to locate
by conventional testing methods.
We have defined some basic principles for runtime detection 
of a class of deadness errors.
These principles apply to a wide class of parallel
programming languages.
We have applied these principles
in an experimental implementation of a runtime monitor for Ada
tasking errors. Initial experiments have demonstrated the feasibility
of applying our runtime monitor techniques {\sl (i)} to debug tasking programs
for deadness errors, and {\sl (ii)} to use evasive action programming techniques
to avoid imminent deadness situations.
These latter techniques are presently under investigation; they constitute
an ability for a system to reconfigure the software when certain critical
situations are recognized.
Reports and publications on runtime monitoring are available
\ref:German.1982. \ref:Helmbold.1983..

\sect References.
\baselineskip 12pt

\makeref:Allen.1970.{Allen, J. R., and Luckham, D. C., \article{An
Interactive Theorem Proving Program,} in \book{Machine Intelligence,}
Michie, Vol. 5, pp. 321, 1970.}

\makeref:Bauer.1978a.{Bauer, F. L., Broy, M., Gnatz, R., Hesse, W., and
Krieg-Brueckner, B., \article{A Wide Spectrum Language for Program
Development,} in \book{Program Transformations,} Third International
Symposium on Programming, edited by Robinet, B., Paris, pp. 1--15, 1978.}

\makeref:Bauer.1978b.{Bauer, F. L., Broy, M., Gnatz, R., Hesse, W.,
Krieg-Brueckner, B., Partsch, P., Pepper, P., and Woessner, H.,
\article{Towards a Wide Spectrum Language to Support Program Specification
and Program Development,} ACM SIGPLAN Notices, Vol. 13, No. 12, pp.
15--24, 1978.}

\makeref:Bauer.1981a.{Bauer, F. L., Broy, M., Dosch, W., Gnatz, R.,
Geiselbrechtinger, F., Hesse, W., Krieg-Brueckner, B., Laut, A., Matzner,
T. A., Moeller, B., Partsch, H., Pepper, P., Samelson K., Wirsing, M., and
Woessner, H., \article{Report on a Wide Spectrum Language for Program
Specification and Development (tentative version),} Institut fuer
Informatik der TU Muenchen, No. TUM-I8104, 1981.}

\makeref:Bauer.1981b.{Bauer, F. L., Broy, M., Dosch, W., Gnatz, R.,
Krieg-Bruckner, B., Laut, A., Luckmann, M., Matzner, T. A., Moeller, B.,
Partsch, H., Pepper, P., Samelson, K., Steinbrueggen, R., Wirsing, M., and
Woessner, H., \article{Science of Computer Programming,} in
\book{Programming in a Wide Spectrum Language:  A Collection of Examples,}
Vol. 1, pp. 73--114, 1981.}

\makeref:Cartwright.1978.{Cartwright, R. and Oppen, D.,
\article{Unrestricted Procedure Calls in Hoare's Logic,} Proceedings of
the Fifth ACM Symposium on Principles of Programming Languages, ACM, New
York, January 1978.}

\makeref:Falis.1982.{Falis, E., \article{Design and Implementation in Ada
of a Runtime Task Supervisor,} Proceedings of the AdaTec Conference on
Ada, ACM, Gargaro, A. B., Arlington, Virginia, pp. 1--9, October 1982.}

\makeref:Finlayson.1982.{Finlayson, R. S., \article{EDT: A Syntax-Based
Program Editor,} 1982.}

\makeref:Flon.1977.{Flon, L., and Suzuki, N., \article{Nondeterminism and
the Correctness of Parallel Programs,} Proceedings IFIP Working Conference
on the Format Description of Parallel Programs, 1977.}

\makeref:German.1975.{German, S. M., and Wegbreit, B., \article{A
Synthesizer of Inductive Assertions,} IEEE Transactions on Software
Engineering, Vol. SE-1, No. 1, pp. 68--75, March 1975.}

\makeref:German.1977.{German, S. M., Luckham, D. C., and Oppen, D. C.,
\article{Extended Pascal Semantics for Proving the Absence of Common
Runtime Errors,} 1977.}

\makeref:German.1978.{German, S., \article{Automating Proofs of the
Absence of Common Runtime Errors,} Proceedings of the Fifth ACM Symposium
on Principles of Programming Languages, ACM, New York, pp. 105--118,
1978.}

\makeref:German.1979a.{German, S., Luckham, D. C., and Oppen, D.,
\article{Proving the Absence of Common Runtime Errors,} 1979.}

\makeref:German.1979b.{German, S., \article{An Automatic system for
Proving the Absence of Common Runtime Errors,} 1979.}

\makeref:German.1979c.{German, S., \article{Verification with Variant
Records, Unions Types, and Direct Access to Data Representations,} 1979.}

\makeref:German.1980.{German, S. M., \article{An Extended Semantic
Definition of Pascal for Proving the Absence of Common Runtime Errors,}
Stanford University, Program Verification Group Report PVG-18,
STAN-CS-80-811, June, 1980.}

\makeref:German.1980.{German, S. M., von Henke, F. W., Luckham, D. C.,
Oppen, D., and Polak, W., \article{Program Verification at Stanford,}
Software Engineering Notes, Vol. 5, No. 3, pp. 13--16, July 1980.}

\makeref:German.1981.{German, S. M., \article{Verifying the Absence of
Common Runtime Errors in Computer Programs,} Stanford University, Program
Verification Group Report PVG-19, STAN-CS-81-866, June 1981.}

\makeref:German.1982.{German, S. M., Helmbold, D. P., and Luckham, D. C.,
\article{Monitoring for Deadlocks in Ada Tasking,} Proceedings of the
AdaTec Conference on Ada, ACM, Gargaro, A. B., Arlington, Virginia, pp.
10--25, October 1982.}

\makeref:Helmbold.1983.{Helmbold, D., and Luckham, D. C.,
\article{Techniques for Runtime Detection of Deadness Errors in Ada
Tasking,} 1983.}

\makeref:Huet.1980.{Huet, G., and Oppen, D. C., \article{Equations and
Rewrite Rules, A Survey,} Academic Press, 1980.}

\makeref:Ichbiah.1979b.{Ichbiah, J. D., Barnes, J. P. G., Heliard, J-C.,
Krieg-Brueckner, B., Roubine, O., and Wichmann, B. A., \article{Rationale
for the Design of the Ada Programming Language,} ACM SIGPLAN Notices, Vol.
14, No. 6, 1979.}

\makeref:Ichbiah.1980.{Ichbiah, J. D., Krieg-Brueckner, B., Wichmann, B.
A., Ledgard, H. F., Heliard, J-C., Abrial, J-R., Barnes, J. P. G.,
Woodger, M., Roubine, O., Hilfinger, P. N., Firth, R., \article{Reference
Manual for the Ada Programming Language: Proposed Standard Document,} US
Department of Defense, US Government Printing Office, Vol.
008-000-00354-8, July 1980.}

\makeref:Ichbiah.1982.{Ichbiah, J. D., Krieg-Brueckner, B., Wichmann, B.
A., Ledgard, H. F., Heliard, J-C., Abrial, J-R., Barnes, J. P. G.,
Woodger, M., Roubine, O., Hilfinger, P. N., Firth, R., \article{Reference
Manual for the Ada Programming Language: Proposed Standard Document,} US
Department of Defense, US Government Printing Office, July 1982.}

\makeref:Igarashi.1975.{Igarashi, S., London, R. L., and Luckham, D. C.,
\article{Automatic Program Verification I:  Logical Basis and its
Implementation,} Acta Informatica, Vol. 4, pp. 145--182, 1975.}

\makeref:Karp.1976.{Karp, R., and Luckham, D. C., \article{Verification
of Fairness in an Implementation of Monitors,} Proceedings of 2nd
International Conference on Software Engineering, IEEE, San Francisco,
California, 40-46, October 1976.}

\makeref:Karp.1979.{Karp, R. A., \article{Proving Concurrent Systems
Correct,} Stanford University, Program Verification Report PV-14,
STAN-CS-79-783, November 1979.}

\makeref:Krieg-Brueckner $\&$ Luckham.1980.{Krieg-Brueckner, B., and Luckham, D. C.,
\article{Anna:  Towards a Language for Annotating Ada Programs,}
Proceedings of the ACM SIGPLAN Symposium on the Ada Programming Language,
Vol. 15, No. 11, pp. 128--138, November 1980.}

\makeref:Krieg-Brueckner.1982a.{Krieg-Brueckner, B., Luckham, D. C., von
Henke, F. W., and Owe, O., \article{Axiomatic Semantics of Anna,} 1982.}

\makeref:Krieg-Brueckner.1982b.{Krieg-Brueckner, B., Luckham, D. C., von
Henke, F. W., and Owe, O., \article{Transformations of Anna to Anna
Kernel,} 1982.}

\makeref:Krieg-Brueckner et al.1982c.{Krieg-Brueckner, B., Luckham, D. C., von
Henke, F. W., and Owe, O., \article{Reference Manual for Anna: A Language
for Annotating Ada Programs,} 1982.}

\makeref:Luckham.1977a.{Luckham, D. C., \article{Program Verification and
Verification-Oriented Programming,} Proceedings of IFIP Congress 77,
North-Holland Publishing Co., Amsterdam, pp. 783--793, August 1977.}

\makeref:Luckham.1977b.{Luckham, D. C., and Suzuki, N.,
\article{Automatic Program Verification IV: Proof of Termination within a
Weak Logic of Programs,} Stanford University, No. AIM-269, 1977.}

\makeref:Luckham.1977c.{Luckham, D. C., and Suzuki, N., \article{Proof of
Termination within a Weak Logic of Programs,} Acta Informatica, Vol. 8,
pp. 21--36, March 1977.}

\makeref:Luckham.1978a.{Luckham, D. C., and Polak, W., \article{A
Practical Method of Documenting and Verifying Programs with Modules,}
1978.}

\makeref:Luckham.1978b.{Luckham, D. C., and Suzuki, N.,
\article{Verification-Oriented Proof Rules for Arrays, Records, and
Pointers,} Stanford University, No. AIM-278, April 1978.}

\makeref:Luckham.1978c.{Luckham, D. C., Morales, J. J., and Schreiber, J.
F., \article{A Study in the Application of Theorem Proving,} Proceedings
of the Conference on Artificial Intelligence and Simulation of Behavior,
Conference on Artificial Intelligence and Simulation of Behaviour,
Hamburg, Germany, pp. 176--188, July 1978.}

\makeref:Luckham.1979a.{Luckham, D. C., and Karp, R. A.,
\article{Axiomatic Semantics of Concurrent Cyclic Processes,} 1979.}

\makeref:Luckham.1979b.{Luckham, D. C. and Suzuki, N.,
\article{Verification of Array, Record and Pointer Operations in Pascal,}
ACM TOPLAS, Vol. 1, No. 2, pp. 226--244, October 1979.}

\makeref:Luckham.1980a.{Luckham, D. C. and Polak, W., \article{Ada
Exception Handling:  An Axiomatic Approach,} ACM TOPLAS, Vol. 2, No. 2,
pp. 225--233, April 1980.}

\makeref:Luckham.1980b.{Luckham, D. C. and Polak, W., \article{A
Practical Method of Documenting and Verifying Ada Programs with Packages,}
Proceedings of the ACM SIGPLAN Symposium on the Ada Programming Language,
Vol. 15, No. 11, pp. 113--122, November 1980.}

\makeref:Luckham.1980c.{Luckham, D. C., and Polak, W., \article{Ada
Exceptions: Specification and Proof Techniques,} Stanford University,
Program Verification Group Report PVG-16, STAN-CS-80-789, February 1980.}

\makeref:Luckham.1981a.{Luckham, D. C., Larsen, H. J., Stevenson, D. R.,
and von Henke, F., \article{ADAM---An Ada-based Language for
Multi-processing,} Stanford University, Program Verification Group Report
PVG-20, STAN-CS-81-867, July 1981.}

\makeref:Luckham.1981b.{Luckham, D. C., and von Henke, F. W.,
\article{Program Verification at Stanford,} Software Engineering Notes,
Vol. 6, No. 3, pp. 25--27, July 1981.}

\makeref:Luckham.1983a.{Luckham, D. C., von Henke, F. W., Larsen, H. J.,
Stevenson, D. R., \article{ADAM: an Ada-based Language for
Multi-processing,} Stanford University, 1983.}

\makeref:Luckham.1983b.{Luckham, D. C., and Falis, E. P., \article{The
Adam Compiler,} 1983.}

\makeref:Nelson.1978a.{Nelson, G., and Oppen, D., \article{A Simplifier
Based on Efficient Decision Algorithms,} Proceedings of the Fifth ACM
Symposium on Principles of Programming Languages, ACM, January 1978.}

\makeref:Nelson.1978b.{Nelson, C., and Oppen, D., \article{Fast Decision
Algorithms based on Congruence Closure,} Stanford University,
STAN-CS-78-646, 1978.}

\makeref:Nelson.1979.{Nelson, G., \article{Techniques for Program
Verification,} Stanford University, 1979.}

\makeref:Oppen.1978a.{Oppen, D., \article{Reasoning about Recursively
Defined Data Structures,} Stanford University, STAN-CS-78-678, 1978.}

\makeref:Oppen.1979.{Oppen, D., \article{Convexity,Complexity, and
Combinations of Theories,} Proceedings of the Fifth Symposium on Automated
Deduction, ACM, January 1979.}

\makeref:Polak.1979.{Polak, W., \article{An Exercise in Automatic Program
Verification,} IEEE Transactions on Software Engineering, Vol. 5, pp.
453--458, September 1979.}

\makeref:Polak.1980.{Polak, W. H., \article{Theory of Compiler
Specification and Verification,} Stanford University, Program Verification
Group Report PVG-17, STAN-CS-80-802, May 1980.}

\makeref:Polak.1981a.{Polak, W., \article{Program Verification Based in
Denotational Semantics,} POPL, January 1981.}

\makeref:Polak.1981b.{Polak, W., \article{Program Verification at
Stanford:  Past, Present, Future,} Proceedings of Workshop on Artificial
Intelligence, Workshop on Artificial Intelligence, January 1981.}

\makeref:Scherlis.1979.{Scherlis, W., \article{A Rule Language and its
Implementation,} 1979.}

\makeref:Stanford Verification Group.1979.{Stanford Verification Group,
\article{Stanford Pascal Verifier User Manual,} Stanford University,
Program Verification Report PV-11, STAN-CS-79-731, March 1979.}

\makeref:Stevenson.1980.{Stevenson, D. R., \article{Algorithms for
Translating Ada Multitasking,} ACM SIGPLAN Notices, Vol. 15, No. 11,
November 1980.}

\makeref:Suzuki.1974.{Suzuki, N., \article{Automatic Program Verification
II:  Verifying Programs by Algebraic and Logical Reduction,} Stanford
University, No. STAN-CS-74-473, 1974.}

\makeref:Suzuki.1976.{Suzuki, N., \article{Automatic Verification of
Programs with Complex Data Structures,} Stanford University, No.
STAN-CS-76-552, 1976.}

\makeref:Suzuki.1977.{Suzuki, N., and Ishihata, K.,
\article{Implementation of an Array Bound Checker,} Proceedings Fourth ACM
Symposium on Principles of Programming Languages, ACM, pp. 132--143,
January 1977.}

\makeref:von Henke.1974.{von Henke, F. W., and Luckham, D. C.,
\article{Automatic Program Verification III: A Methodology for Verifying
Programs,} Stanford University, Program Verification Number PV-3,
Stan-CS-74-474, AIM-256, December 1974.}

\makeref:von Henke.1982.{von Henke, F., \article{A Strongly Typed
Language for Specifying Programs, } 1982.}

\vfill\eject

%Analysis of Algorithms
\ctrline{RESEARCH IN THE ANALYSIS OF ALGORITHMS AND ARCHITECTURES}

$$\vcenter{\halign{\lft{#}\cr
Gene Golub, Professor\cr
Computer Science Department\cr
Stanford University\cr}}$$
 
\initsect

\sect Introduction.
\save6\hbox{\count0}

The Stanford research group for the analysis and construction of algorithms 
for both combinatorial and numerical/scientific problems is interested
in relating problems and algorithms to computer architectures.

\sect Synergic Approach.

Most of the research relating computational problems to computer
architectures has been ad hoc and few principles have emerged.
Architectures are presented and analyzed in terms of a few benchmark
problems.  They are presumably engineering solutions to computational
needs---a solution to a problem.  However, the identity of the problem
that a given architecture is engineered for is almost never stated.
Similarly, the customers submit benchmarks which are almost meaningless to
the architects in terms of language and often simplified in a manner which
belies the computational requirements of the customers.  In fact, most of
these customers would find a machine which was optimal for their
benchmarks to be wholly inadequate for their needs.  Additionally, most of
the algorithmic effort has been to shoehorn known algorithms onto new
machines rather than pursue a synergic approach.

We wish to develop some measures that gauge realistic tasks and that can
describe and evaluate the the tools that are brought to bear on these
tasks.

Some steps in this direction are:

\numitem{1.}Developing algorithm-independent results on the complexity
and topology of representative applications;

\numitem{2.}Obtaining lower bounds on the optimal ratio of processer power
to communication capability for representative problems;

\numitem{3.}Relating algorithmic requirements in terms of topology, data rates,
and processor capability to physical and technological restrictions;

\numitem{4.}Investigating inherent tradeoffs in convergence rates and complexity
with concurrancy.

\numitem{5.}Considering a metalanguage for the description of applications
problems in terms of standard computational processes which expresses
both the complexity of the computation and its topology,
and which allows accurate simulation of the process
for various architectures.  This effort would provide a means of
description of problem environments from the users point of view
and a description of the applications class for which a machine
is posed as a reasonable solution.

\vfill\eject
%Vision and Robotics
\ctrline{INTELLIGENT SYSTEMS}
\ctrline{FOR} 
\ctrline{COMPUTER VISION AND ROBOTICS}

$$\vcenter{\halign{\lft{#}\cr
Thomas Binford, Professor of Computer Science (Research)\cr
Computer Science Department\cr
Stanford University\cr}}$$
 
\initsect
\sect Introduction.
\save7\hbox{\count0}

This effort aims to understand and build integrated, intelligent computer
systems with these components:  perception; representation;
reasoning and planning; learning and memory; programming systems and user
interfaces; sensory technology based on computers; and output devices and
their control.  The research will build on a strong base, an existing
system, ACRONYM, which is in use at about 10 laboratories.  Intelligent
systems research is aimed toward applications to Image Understanding
including stereo mapping, navigation of autonomous vehicles, military
robotics, manufacturing, and automatic programming of real-world tasks.

Practical considerations dictate profound imaging science to build systems
which are not dead-end, engineered for a special demonstration, but extend
to realistic operational requirements.

\ssect Motivation.

An intelligent system must have high performance in terms of functionality
and response time and must be accessible to its users.  The group has
focused on building the ACRONYM system and its SUCCESSOR as integrated
systems which use available knowledge, sensory data, and perceptions in
reasoning, planning, and interpretation.  This is primarily a problem of
science, not system building.  Fundamental advances are required for
components and for their integration.

An intelligent system with high functionality must use all available
knowledge and data from many diverse sources and must use it well.  To
utilize multi-sensory data combined with expert knowledge and diverse
information requires effective representation of world states in
space/time, the relation between world states, and operations as
transitions between states.  To use the knowledge and data well means
careful attention to the accurate meaning of constraints and measurements,
and to conclusions to be drawn from them:  How are states constrained by
measurements and knowledge (representation), how tightly are they
contstrained (estimation), and what can be concluded about other states
(representation).  Perception to identify world states, that is, to turn
sensory data into information about world states, requires models of the
observation process including sensors and environment---e.g.
illumination---and requires profound operations to generate structural,
symbolic models of spatial data or images.  These perceptual operations of
segmentation and aggregation yield geometric and photometric models (or
intensity for tactile or other sensors).  Perceptual inference rules
provide relationships of several sorts:  1) between geometric relations in
data and intrinsic geometric properties of surfaces (shape from shape); 2)
between photometric or intensity data and intrinsic properties of
surfaces, including geometry and reflectivity of surfaces (shape from
shading or texture), or mechanical properties, for instance, deformability
or stiffness from touch intensity.

To make an intelligent system accessible to users requires a major programming
system which includes:

\numitem{1.}an intelligent, rule-based user interface with
geometric input and output devices, and image input;

\numitem{2.}natural language input (application of natural language, not research in 
natural language;

\numitem{3.}learning based on inference rules for inferring spatial models;
for example, most input is two-dimensional or one-dimensional (space
curves) meant to be interpreted as three dimensional objects; learning of
behavior is acquiring inference rules for space/time models;

\numitem{4.}models of the user;

\numitem{5.}expert knowledge;

\numitem{6.}database mechanisms; and

\numitem{7.}automatic programming, generation of perceptual strategies.

In order to make intelligent systems which respond quickly enough,
efficient coding is a minor advance.  Orders of magnitude improvement
are required typically for those cases for which we know solutions at all.
Such advances come from:

\numitem{1.}problem simplification using special case information; providing general
methods to use special case information;

\numitem{2.}building fast computers; understanding VLSI technology and architecture
of vision algorithms;

\numitem{3.}automatically determining strategies to cut the computational complexity
of vision algorithms; understanding the architecture of vision algorithms.

In this domain geometric and physical information are central.  Physics
is represented in geometric terms.  Thus the representation of geometry is
central to this effort.  Further, we make the strong claim that other
representations, all representations, are based on mechanistic analogy
with physics and mathematical representations, especially geometry.  That
is, social and psychological models are essentially mechanistic analogies.
Under this assumption, representation of geometry is the basis for all
intelligence and reasoning.

\sect Research Topics.

Intelligent actors or robots incorporate input, planning, and output; or
sensing, intelligence, and action.  Research covers this spectrum.  This
research focuses on intelligence, embodied in the ACRONYM system and its
successor.  As a preliminary, sensors and action devices will be discussed
first.

Research in sensing includes computational methods in sensory technology,
application of novel sensing methods, and, where necessary, device
technology.  Sensor systems under investigation in collaboration with
other groups at Stanford and elsewhere include force and touch sensors for
robots, acoustic imaging sensors, and smart optical sensors.  Application
of sensors to mobile robots and to precision manufacturing are being
explored.

Research in action devices includes building effectors, controlling them,
and programming them with traditional language systems.  Research is aimed
at building hands and arms which can make secure grasps, use tools, or
exert delicate forces for assembly, which enable generic operations of
parts acquisition, parts transfer, and parts mating.  This research is
carried out in collaboration with other groups on campus and nationwide,
especially MIT, JPL, and the University of Utah.  Control studies include:
control of coupled, complex systems such as a three-finger hand with nine
degrees of freedom; task level control of devices in terms of position,
velocity, and forces on objects, not joint coordinates of devices;
estimation of dynamic properties of devices; adaptive control; fundamental
limits of force control, and force control in parts mating.  One goal is
to move loads as rapidly and smoothly as possible under sensor control.
Force control is embedded in a high level language, AL, for explicit
programming of assemblies.  Research is pursued in debugging real-time
devices, user interfaces, specification of tasks, concurrency and
synchronization, error recovery and exception handling.  A large
integrated robot system is implemented in AL.

\sect Intelligence.

The focus of this project is on intelligence, a domain with enormous scope.

An aspect of the research is study of the architecture of vision algorithms
and their implementation in integrated circuits (VLSI) to achieve
real-time performance, i.e. fast enough to be useful in applications.
This study includes fault tolerant design.  Most research has been aimed
at image processing algorithms, but the intention here is to study 
implementation of high levels of perception and reasoning in high performance
VLSI.

One goal is to introduce structural learning mechanisms into ACRONYM, to
learn object models and object classes, to learn rules and strategies,
i.e. programs, and to learn when to use what it has learned.  Building the
knowledge base or rule bases which capture the knowledge of experts
consumes great effort.  A central concern is learning from one example or
few, learning causal relations in distinction to statistical correlations,
because causal relations define decision criteria which are dependable.
In contrast, decisions based on statistical distributions are often
unreliable because of systematic bias.

Representation is a central issue in defining similarity classes of
objects.  It is argued that fundamental definitions of object classes
are functional, that function $=$ form \ref:Binford.1982..
An essential part of learning is relating function and structure.

\ssect Perception.

Perception research aims to extend monocular cues to object interpretation
and figure/ground  discrimination.  It  is computationally  infeasible  to
attempt to match all combinations of features against models.
Instead, it is important to group image features in canonical ways. 
Segmentation and aggregation are complementary processes which discriminate
features and group them.  Some grouping is suggested by image structure,
corresponding to figure/ground discrimination.  

Other groupings arise from three dimensional interpretation of images.
This is known as inferring shape from shape: three dimensional 
shape from two dimensional shape.   Inference rules guide the estimation
of surface discontinuities (obscuration), surface tangent discontinuities
(edges), surface orientation, and surface curvature.  Inference rules for
the interpretation of shadows is also a topic for exploration.

Research has been pursued on geometric constraints in stereo vision.
These constraints are the key to building effective stereo mapping systems
which might serve the needs of the Defense Mapping System.  They include
traditional mechanisms for stereo correspondence but introduce much new
monocular interpretation.  The basic theme is to integrate all constraints,
general and specific.

Two major themes are
multi-sensor integration with collateral information and knowledge bases, and
interpretation of images by matching with generic and specific models.

\ssect Geometric Modeling and Geometric Reasoning.

Geometric reasoning mechanisms include the rule language for
expression of rules, the rule base for transforming constraints
into algebraic constraints, symbolic manipulation routines for
performing geometric transforms and simplification to derive
symbolic prediction expressions with variables, constraint resolution
mechanisms to test satisfiability of constraint systems,
statistical constraint propagation with symbolic expressions.

Two major areas of research are problem formulation and
generation of efficient strategies.  Problem formulation will 
enable stating and solving problems such as finding efficient algorithms
for determining convex hulls and similar problems from computational
geometry.

\ssect Representation.

In geometric modeling, ACRONYM is based on generalized cylinder representation
for solids.  Complementary representations of surfaces, edges, and vertices
are being introduced, together with meta-representation of geometric types.
Representations of kinematics of joints and assemblies are under investigation.
Graphics methods are explored for broader classes of generalized
cylinders.  

The representation of physics in an intelligent system is under
investigation.  Physics makes an identification between physical
structures and geometric structures, for example, representing positions
as vectors, and an identification between physical actions and geometric
maps, for example, rotations as orthogonal transformations.  Sensors and
observation will be modeled along with kinematics and dynamics.

Physical object classes are not defined by three-dimensional shapes, but
by function.  Mechanisms will be implemented for representing function as
structure.  One aspect of function is fabrication, representing
fabrication processes.

The representation of space/time sequences in intelligent systems makes
use of the same mechanisms as the representation of space.  The
representation of time assumes events and an observer with an internal
clock, i.e. a mechanism for judging before and after with an internal
metric.  Coordinate transformations relate time frames.  Events may be
continuous or discrete.  Parallelism and synchronization are represented
by constraints.

Geometry serves as the underlying representation for the physical world
and as the underlying representation for implementation of the intelligent
system.  Relations will be represented among many levels of geometric
types which include real numbers, tuples, vectors, points, curves,
surfaces, and volumes; we plan to represent maps among these types.
Programs which manipulate geometric structures can be represented as maps.
A system that reasons about geometry should understand the structural
relationships among geometric types in order to formulate and generate
programs which solve geometric problems.  In order to reason by analogy, a
system should understand geometric programs in a deep way.

\ssect Applications.

Development of a robot is underway which builds its own model of a
changing environment, which is intended to have high performance acoustic
imaging and stereo vision, and which has intelligent task planning.

Expert systems are being developed for Image Understanding, for robotics, 
and for manufacturing.

Development is underway of a next generation robot programming language
based on geometric reasoning in ACRONYM, with geometric modeling, use of
a computer-aided design data base, planning and problem solving,
mechanisms for integration of vision and other sensing, off-line
programming with simulation, and a hierarchy of language and computer
systems (maxi, mini, micro).  This includes automating choice of grasping
positions, extending collision avoidance, automating the use of sensing in
verification of robot actions, and automating translation of constraints
into positions and forces in parts mating.

Intelligent systems are under investigation for computer-aided mechanical
design, based on the ACRONYM system.  CAD as now practiced is
computer-aided drafting and archiving.  This study concerns creative
design.  An objective is a fast turnaround prototyping fabrication
facility.  A study will be made of synthesis of mechanical designs using
the specification of design constraints in terms of function and the
relation of function to structure \ref:Lowry.1982., and methods of testing
constraint satisfaction.  

\sect Accomplishments.

Recent research has centered on the ACRONYM system, an
intelligent, knowledge-based system for vision and planning 
\ref:Brooks.1979. \ref:Brooks.1981..
It integrates subsystems for interaction with users, for interaction
with the world, for modeling the world, and subsystems for planning,
interpretation, and decision making.  ACRONYM contains a substantial core
of fundamental mechanisms which are powerful and general.  Its performance
demonstrated thus far depends on domain-independent capabilities, not on
special domain-dependent tricks.  ACRONYM incorporates geometric modeling
with rule-based geometric reasoning.

Recognition of aircraft has been demonstrated in ACRONYM.
ACRONYM has been used as a central part of a major  ARPA project and has
been distributed to about 10 research groups.

Recent efforts have gone towards SUCCESSOR, a follow-on to ACRONYM.
The modeling system is being extended to include negative volumes,
multiple instances of objects, and a general name-scoping mechanism.
The representation of shape is being extended to
a very general subclass of generalized cylinders.  A powerful graphics
display system is being built.  A large set
of aircraft models have been built.  With these, some problems with the rule
set for recognition have been discovered, and the constraint resolution
system has been tested.

\ref:Malik.1982. described representation of space/time as constraint
systems and efficient methods for resolution of constraints.  A joint
effort with MIT produced preliminary results in learning which relates
object function to form \ref:Winston.1983.\ref:Lowry.1982..  This work is
a step toward learning of object classes and learning of production rules,
i.e. procedures, by combining geometry in ACRONYM and work relating
function and structure at Stanford with work at MIT on learning by analogy
and a natural language input system.

Early work led to the representation of objects by generalized cylinder
primitives \ref:Binford.1971., and showed methods of calculating generalized
cylinder representations from surface data \ref:Agin.1972.\ref:Nevatia.1974..

\ref:Agin.1972. described parts of complex objects as generalized
cylinders with circular cross sections.  \ref:Nevatia.1974. built a system
which recognized complex objects including dolls, toy horses, and tools.
The system demonstrated ``learning by showing'' in three dimensions:  it
built models of objects shown to it on a table, then recognized objects
when they were presented in different orientations with different
articulation and some obscuration.  They introduced new concepts for
segmenting complex objects into parts, for building part/whole models of
complex objects as structures of generalized cylinders.  For efficient
matching to models, they used coarse stick figure descriptions to select
subclasses of similar objects for detailed matching.\

\ref:Baumgart.1974. built GEOMED, a geometric modeling system based on a
polyhedral representation, using Euler's theorem and a ``winged edge''
representation.  GEOMED was named for its powerful, interactive geometric
editor.

Recent theoretical results outline a general theory of interpretation of 
line drawings which promises to include arbitrary numbers of curved surfaces
with surface markings and shadows, paper (non-solids), cracks, and wires
\ref:Binford.1981.. These results suggest general rules for inferring whether
surfaces are planar, or if not planar, for inferring their curvature.
Results also show effective means for using shadows as human interpreters do
\ref:Lowe.1981.. 

\ref:Lowe.1982.\ref:Binford.1982. describe extensions of this approach
to general methods for grouping of image features as ribbons and
grouping operations for continuous curves.  These methods address the
figure/ground problem; they are central to subsequent recognition.
reconstruction of three-dimensional shapes based on shadows;
They also present preliminary results in finding clusters
of dots, edges, and texture elements.  

\ref:Miller.1982b. describe architecture studies aimed at development of
an array of 128$\times$128 bit-serial general purpose processors in wafer
scale integration.  There is a large probability that some of the
processors will be faulty.  Such a large circuit requires fault tolerant
design.  They demonstrate an algorithm for connecting the array around
defective processors, an algorithm effective for up to 10$\%$ defective
processors.  They describe software experiments used to explore issues of
architecture.  Previously, \ref:Miller.1981. designed, implemented, and
tested one working element of the array. SAIL has surveyed hardware
implementation of vision algorithms.

The group made a comprehensive survey of stereo systems and available
techniques.  The group has a major effort underway to implement and
integrate all available constraints and knowledge, general and special,
monocular and stereo, within a comprehensive, rule-based stereo
interpretation system.  Most of these constraints, especially monocular
cues, have not been included in any previous stereo system; all others use
only a few, simple conditions.  The constraints of \ref:Arnold.1980. have
been included in a system with a dynamic programming search process
\ref:Arnold.1983..  Geometric constraints include:  1) angles of
corresponding views of a vector; 2) projections of corresponding views of
a surface; a necessary condition for obscuration; and 3) views of opaque
surfaces.

The system of \ref:Baker.1981. has been extended to include the difficult
case in which images do not correspond along scan lines.  It has been
modified to use edge data from \ref:Marimont.1982..  In order to calculate
stereo geometry in a sufficiently general way, a new system for stereo
registration has been developed.  A new search method for stereo
registration was developed \ref:Clarkson.1981..  Currently, the group is
designing generic models of buildings to serve in a rule-based system
which incorporates monocular and stereo inference rules based on
\ref:Binford.1981.\ref:Lowe.1981..  Preliminary results have been obtained
in using cube corners, horizontal surfaces, and horizontal edges in stereo
correspondence, going beyond the results of \ref:Liebes.1981..

A kinematic simulator was made for robots, based on ACRONYM \ref:Soroka.1980..
A dynamic simulator for mechanical system has been built.
A rule  base  for
automated grasping in ACRONYM was made in  1979. 

Extensive experimentation has been carried out 
with touch sensing \ref:Binford.1972..  The Scheinman force  sensor was developed;
it has  been widely  distributed.  Force sensing fingers have been developed.

The group developed the AL system for programming robots, developed an
integrated experimental robotics system based on AL, then made a portable
version.  There are three other implementations based on AL, at Karlsruhe,
Tokyo Univ, and Univ of Grenoble.

SAIL designed and built the Scheinman Stanford arm in 1970 and the
Stanford-JPL three finger hand \ref:Salisbury.1981..  Both have had
significant impact outside Stanford; several laboratories are buying
copies of the Stanford-JPL hand.  The Salisbury hand and Okada's hand at
ETL, Japan represent the state of the art.  A hydraulic arm was built in
1968; Scheinman built the Stanford arm in 1970.  Paul implemented WAVE in
1971, the first programming system to provide several modern mechanisms.
The VAL programming system of Unimation was based on WAVE; Bruce Shimano,
formerly of this laboratory, has led VAL development since its inception.

The arm and WAVE were combined in the first 
computer integrated assembly, the assembly of an automobile  water
pump from 10 component  parts \ref:Paul.1973.\ref:Bolles.1973., 
using force and touch sensing extensively along with vision, 
a power  tool, and several fixtures.

\ref:Salisbury.1981. made a sophisticated theory for coupled control of
the three finger hand using tension sensors.  The hand has three fingers,
each with three degrees of freedom.  The control commands the position,
velocity and internal force on an object to be grasped by the hand, rather
than command individual motors for nine joints.  The same analysis is
relevant for two arms cooperating or other closed loop kinematic chains.
In the past SAIL implemented compliance and force control based on a
general analysis \ref:Salisbury.1980..  \ref:Khatib.1983. has implemented
a Cartesian force control system, with real-time collision avoidance.  The
Cartesian system facilitates real-time collision avoidance.  The Cartesian
force control system has no known rivals.  Collision avoidance has been
investigated by \ref:Widdoes.1974..

SAIL has studied
navigation of mobile robots \ref:Schmidt.1972.\ref:Moravec.1980..  A mobile robot
demonstrated navigation around obstacles in realistic interior and external 
environments, using stereo vision.
\sect References.
\baselineskip 12pt

\makeref:Agin.1972.{Agin, G.J.,
\article{Representation and Description of Curved Objects}
AI Lab, Stanford University, Memo AIM-173, CS-305, 1972.}

\makeref:Arnold.1977.{Arnold,R.D.; \article{Spatial Understanding}
Proc Image Understanding Workshop, April 1977.}

\makeref:Arnold.1978.{Arnold,R.D.; \article{Local Context in Matching Edges for Stereo
Vision}; Proc Image Understanding Workshop, Boston, May 1978.}

\makeref:Arnold.1980.{Arnold, R.D., Binford, T.O.;
\article{Geometric Constraints in Stereo Vision}
Proc SPIE Meeting, San Diego, Cal, July 1980.}

\makeref:Arnold.1983.{R.D.Arnold;
thesis, Stanford AI Lab, 1983.}

\makeref:Bajcsy.1972.{Bajcsy, R.;
\article{Computer Identification of Textured Visual Scenes},
Artificial Intelligence Laboratory, Stanford University, Memo
AIM-180, October 1972.}

\makeref:Baker.1980.{Baker, H.;
\article{Edge-Based Stereo Correlations};
Proc Image Understanding Workshop, Baltimore, April l980.}

\makeref:Baker.1981.{Baker, H. and Binford, T.O.;
\article{Depth from Edge and Intensity Based Stereo};
Proc Int Joint Conf on AI, Aug 1981.}

\makeref:Baker.1982.{Baker, H.;    
\article{A system for automated stereo mapping};
Proc. IU Workshop Image Understanding  September 1982.}

\makeref:Baumgart.1974.{Bruce Baumgart;
\article{Geometric Modeling for Computer Vision};
AI Lab, Stanford University, Memo AIM-249, 1974.}

\makeref:Binford.1971.{T. O. Binford;
\article{Computer Visual Perception};
Invited Paper, Systems, Man and Cybernetics Conf, Miami, Fla, 1971.}

\makeref:Binford.1974.{T. O. Binford et al;
\article{Exploratory Study of Computer Integrated Assembly Systems};
AI Lab, Stanford University, 
First Report, 1974.}

\makeref:Binford.1976.{T. O. Binford et al;
\article{Exploratory study of Computer Integrated Assembly Systems};
AI Lab, Stanford University, Third Report, 1976.}

\makeref:Binford.1981.{Binford, T. O.;
\article{Inferring Surfaces from Images};
Artificial Intelligence Journal August, 1981.}

\makeref:Binford.1982.{T.O.Binford;
\article{Segregation and Aggregation: the Figure/Ground problem};
Proceedings of the Rank Prize Fund Conf on Machine and Biological Processing
of Images.}

\makeref:Bolles.1973.{Robert Bolles, Richard Paul;
\article{The use of Sensory Feedback in a Programmable Assembly Systems};
AI Lab, Stanford University,
Memo AIM-220, 1973.}

\makeref:Bolles.1976.{Robert C. Bolles,
\article{Verification Vision Within a Programmable Assembly System};
AI Lab, Stanford University,
Memo AIM-295, 1976.}

\makeref:Brooks.1979.{R. Brooks, R. Greiner, T. O. Binford;
\article{ACRONYM: A Model-Based Vision System};
Proc Int Jt Conf on AI, Tokyo, Aug 1979.}

\makeref:Brooks.1979b.{Brooks, R.A.;
\article{Goal-Directed Edge Linking and Ribbon Finding};
Proc Image Understanding Workshop, Palo Alto, Calif, Apr 1979.}

\makeref:Brooks.1981.{R. Brooks;
\article{Symbolic Reasoning among 3-D Models and 2-d Images};
Artificial Intelligence Journal, August 1981.}

\makeref:Clarkson.1981.{Clarkson, K. L.;
\article{A Procedure for Camera Calibration};
Proc Image Understanding Workshop, April 1981.}

\makeref:Finkel.1974.{R. Finkel, R. H. Taylor, R. C. Bolles, R. Paul, 
and J. A. Feldman;
\article{AL, A Programming System for Automation}; Memo AIM-243;
AI Lab, Stanford University, 1974.}

\makeref:Gennery.1977.{Gennery, D. B.;
\article{A Stereo Vision System for An Autonomous Vehicle};
Proc 5th International Joint Conf on Artificial Intelligence,
MIT, Boston, Aug 1977.}

\makeref:Gennery.1979.{Gennery, D. B.;
\article{Object Detection and Measurement using Stereo Vision};
Proc Int Joint Conf on AI, Aug 1979.}

\makeref:Gennery.1980.{Gennery, D. B.;
\article{Modeling the Environment of an Exploring Vehicle by means of Stereo Vision};
AI Lab, Computer Science Dept, Stanford Univ, 1980.}

\makeref:Goldman.1983.{Ron Goldman;
\article{Design of an Interactive Manipulator Programming Environment};
Memo AIM-350, Stanford University, 1982.}

\makeref:Grossman.1976.{David D. Grossman;
\article{Monte Carlo Simulation of Tolerancing in Discrete Parts Manufacturing
 and Assembly};
Memo AIM-280,
AI Lab, Stanford University, 1976.}

\makeref:Hannah.1974.{Hannah, M. J.;
\article{Computer Matching of Areas in Stereo Images}
Artificial Intelligence Laboratory, Stanford University, Memo
AIM-239 1974.}

\makeref:Hueckel.1969.{M. Hueckel;
\article{An Operator which locates edges in digitized pictures};
J.Assoc Computing Mach, 1969.}

\makeref:Hueckel.1973.{Hueckel, M.;
\article{A Local Visual Operator which Recognizes Edges and Lines};
J.Assoc Computing Mach, 20,634 (1973).}

\makeref:Horn.1972.{B. Horn;
\article{The Binford-Horn Edge Finder};
MIT AI Memo 172, 1972.}

\makeref:Khatib.1983.{O. Khatib;
\article{Dynamic Control of Manipulators in Operational Space};
submitted to IFTOMM Congress, 1983.}

\makeref:Liebes.1981.{Liebes, Jr., S.;
\article{Geometric Constraints for Interpreting Images of
Common Structural Elements: Orthogonal Trihedral Vertices};
Proc Image Understanding Workshop, April 1981.}

\makeref:Lowe.1981.{Lowe, D. and Binford, T. O.;
\article{The Interpretation of Three-Dimensonal Structure from Image Curves};
Proc Int Joint Conf on AI, Aug 1981.}

\makeref:Lowe.1982.{D. Lowe, T. Binford;
\article{Segmentation and Aggregation};
Proc ARPA IU Workshop, 1982.}

\makeref:Lowry.1982.{M. Lowry;
\article{Relating Structure and Function};
Proc ARPA IU Workshop, 1982.}

\makeref:Lowry.1982b.{M. Lowry, A. Miller; \article{Analysis of Low-level
Computer Vision Algorithms for Implementation on a VLSI Processor Array},
Proc.\ ARPA Image Understanding Workshop, Stanford University, Stanford
CA., September 1982, 315--322.}

\makeref:Miller.1981.{Miller, A. and Lowry, M.;
\article{General purpose VLSI chip with fault tolerant hardware
for image processing};
Proc Image Understanding Workshop, April 1981.}

\makeref:Miyamoto.1975.{E. Miyamoto, T. O. Binford;
\article{Display Generated by a Generalized Cone Representation};
Conf on Computer Graphics and Image Processing, Anaheim,
Cal, 1975.}

\makeref:Moravec.1977.{Moravec, H. P.;
\article{Towards Automatic Visual Obstacle Avoidance};
Proc 5th International Joint Conf on Artificial Intelligence,
MIT, Boston, Aug 1977.}

\makeref:Moravec.1979.{Moravec, H. P.;
\article{Visual Mapping by a Robot Rover},
Proc Int Joint Conf on AI, Aug 1979.}

\makeref:Moravec.1980.{Moravec, H. P.;
\article{Obstacle Avoidance and Navigation in the Real World by a Seeing Robot Rover};
AI Lab, Computer Science Dept, Stanford Univ, 1980.}

\makeref:Nevatia.1974.{Nevatia, R.;
\article{Structured Descriptions of Complex Curved Objects for Recognition and
Visual Memory}
AI Lab, Stanford University, Memo AIM-250, CS-464, 1974.}

\makeref:Nevatia.1976.{Nevatia, R. K.;
\article{Depth Measurement by Motion Stereo}; Comp. Graph. and Image Proc.,
vol.5 , 1976, pp. 203-214.}

\makeref:Ohwovoriole.1980.{Ohwovoriole,Morgan;
\article{An Extension of Screw  Theory and  
its Application  to the  Automation of  of Industrial Assemblies};
Ph. D. Thesis, Dept Mech Eng, Stanford University, 1980.}

\makeref:Paul.1972.{Richard Paul;
\article{Modelling, Trajectory Calculation and Servoing of a Computer Controlled 
 Arm}; Memo AIM-177,
AI Lab, Stanford University, 1972.}

\makeref:Paul.1973.{Richard Paul, Karl Pingle, and Bob Bolles; \article{Automated Pump
   Assembly}; 16mm color film,
AI Lab, Stanford University, 1973.}

\makeref:Paul.1976.{R. Paul and B. Shimano;
\article{Compliance and Control};
Joint Automatic Controls Conf, Purdue Univ, July 1976.}

\makeref:Pieper.1968.{Donald L. Pieper;
\article{The Kinematics of Manipulators under Computer Control};
Memo AIM-72,
AI Lab, Stanford University, 1968.}

\makeref:Salisbury.1980.{Salisbury, J. K.;
\article{Active Stiffness Control of a Manipulator in Cartesian Coordinates};
Proc 19th IEEE Conference on Decision and Control, Albuquerque, l980.}

\makeref:Salisbury.19and Craig.{Salisbury, J. K. Craig, J.;
\article{Articulated Hands: Force Control and Kinematic Issues};
Proc JACC, Charlottesville, Va, 1981.}

\makeref:Soroka.1980.{Soroka, B. I.;
\article{Debugging Robot Programs with a Simulator};
Proc CADCAM-8 Conference, Anaheim, CA,  l980.}

\makeref:Shimano.1978.{Bruce E. Shimano;
\article{The Kinematic Design and Force Control of Computer Controlled
Manipulators};
Stanford AI Lab Memo AIM 313,  1978.}

\makeref:Shirai.1971.{Y. Shirai and M. Suwa;
\article{Recognition of Polyhedrons with a range finder};
Proc Int Jt Conf on AI, London, 1971.}

\makeref:Taylor.1976.{Russell Taylor;
\article{Synthesis of Manipulator Control Programs From Task-Level Specifications};
Memo AIM-282, 
AI Lab, Stanford University, 1976.}

\makeref:Widdoes.1974.{L. C. Widdoes;
\article{A Heuristic Collision Avoider for the Stanford Arm};
Internal Note,
AI Lab, Stanford University, 1974.}

\makeref:Winston.1983.{P. Winston, T. Binford, B. Katz, M. Lowry
\article{<In Preparation>};
Stanford AI Memo , MIT-AI memo, 1983.}

\vfill\eject
%Table of Contents
\output{\baselineskip 18pt\page\ctrline{\curfont a i}}
\baselineskip 30pt
\vskip 3truein
\:<
\ctrline{Table of Contents}
\vskip 1.5truein
\hbox to size{\hfill Page}

\contents{Introduction}{\box0}
\contents{Basic Research in Artificial Intelligence and Formal Reasoning}{\box1}
\contents{Deductive Programming}{\box2}
\contents{Research in the Analysis of Algorithms}{\box3}
\contents{Management and Use of Knowledge}{\box4}
\contents{Research and Development in Advanced Programming Environments}{\box5}
\contents{Research in the Analysis of Algorithms and Architectures}{\box6}
\contents{Intelligent Systems for Computer Vision and Robotic}{\box7}
\contents{Budget}{Appendix A}

\vfill\end